blob: d3e98ae4d34994801c55da67a75a1794d4cead2f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Definition T:=nat.
Definition le:=Peano.le.
Hints Unfold le.
Lemma le_refl:(n:nat)(le n n).
Auto.
Qed.
Require Le.
Lemma le_trans:(n,m,k:nat)(le n m) -> (le m k) -> (le n k).
EAuto with arith.
Qed.
Lemma le_antis:(n,m:nat)(le n m) -> (le m n) -> n=m.
EAuto with arith.
Qed.
|
