blob: e9dba1e3f81d59104a65b7b1675d45d9a434eb61 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
Inductive Le : nat->nat->Set :=
LeO: (n:nat)(Le O n)
| LeS: (n,m:nat)(Le n m) -> (Le (S n) (S m)).
Parameter iguales : (n,m:nat)(h:(Le n m))Prop .
Type <[n,m:nat][h:(Le n m)]Prop>Cases (LeO O) of
(LeO O) => True
| (LeS (S x) (S y) H) => (iguales (S x) (S y) H)
| _ => False end.
Type <[n,m:nat][h:(Le n m)]Prop>Cases (LeO O) of
(LeO O) => True
| (LeS (S x) O H) => (iguales (S x) O H)
| _ => False end.
Parameter discr_l : (n:nat) ~((S n)=O).
Type
[n:nat]
<[n:nat]n=O\/~n=O>Cases n of
O => (or_introl ? ~O=O (refl_equal ? O))
| (S O) => (or_intror (S O)=O ? (discr_l O))
| (S (S x)) => (or_intror (S (S x))=O ? (discr_l (S x)))
end.
|
