blob: d0ad6a5e255895bc5c9d2c865b763f5e7300667f (
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
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
Definition T:=nat.
Definition le:=Peano.le.
Hints Unfold le.
Lemma le_refl:(n:nat)(le n n).
Auto.
Save.
Lemma le_trans:(n,m,k:nat)(le n m) -> (le m k) -> (le n k).
Unfold le.
Intros.
Generalize H.
Clear H.
Elim H0.
Auto.
Auto.
Save.
Lemma le_mono_S : (n,m:nat)(le n m) -> (le (S n) (S m)).
Unfold le.
NewInduction 1.
Auto.
Auto.
Save.
Hints Resolve le_mono_S.
Lemma le_pred_mono : (n,m:nat) (le n m) -> (le (pred n) (pred m)).
Unfold le.
Induction 1.
Auto.
Intro.
Case m0.
Auto.
Intro.
Simpl.
Auto.
Save.
Hints Resolve le_pred_mono.
Lemma le_S_mono : (m,n:nat)(le (S n) (S m)) -> (le n m).
Intros.
Change (le (pred (S n)) (pred (S m))).
Auto.
Save.
Hints Resolve le_S_mono.
Lemma le_antis:(n,m:nat)(le n m) -> (le m n) -> n=m.
NewInduction n.
Intros.
Inversion H0.
Reflexivity.
Intros.
Inversion H.
Auto.
Rewrite (IHn m0).
Auto.
Rewrite <- H2 in H.
Auto.
Rewrite <- H2 in H0.
Auto.
Save.
|
