blob: 1d5e3fb4e4b5b62d31aa21eccdb0462669ed136f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m :=
[m:nat]
<[n,m:nat] n=m \/ ~n=m>Cases n m of
O O => (or_introl ? ~O=O (refl_equal ? O))
| O (S x) => (or_intror O=(S x) ? (discr_r x))
| (S x) O => (or_intror ? ~(S x)=O (discr_l x))
| ((S x) as N) ((S y) as M) =>
<N=M\/~N=M>Cases (eqdec x y) of
(or_introl h) => (or_introl ? ~N=M (f_equal nat nat S x y h))
| (or_intror h) => (or_intror N=M ? (ff x y h))
end
end.
|
