The Coq mailing list

["" <judy AT mail.ccnu.edu.cn>]

Dear Professer:
how to specify such definitions:

when x=5 ,y=3;
when x=4 , y=m;
when x<>4,x<>5.
P is true.

can I specify them this 2 ways
1
x y m :nat.
P(x y m:nat):Prop:=
 (x=5/\y=3)
 \/(x=4/\y=m)\/(x<>4/\x<>5).

2
x y m k:nat.
P(x y m:nat):Prop:=
 (x=5->y=3)
 /\(x=4->y=m)
  /\(x<>4)/\(x<>5).

how to represent  the  meaning of "else",I can only  use the way (x<>4)(x<>5).

Judy