diff options
| author | filliatr | 2000-03-21 18:53:42 +0000 |
|---|---|---|
| committer | filliatr | 2000-03-21 18:53:42 +0000 |
| commit | b1dab9e06d9a964b1dd0d09bca797cb4a4e4b9a1 (patch) | |
| tree | 1c67698f4b19b4e14774b19a375e40fd009d39a9 /theories | |
| parent | 9a913a2aa1834704908ec829d5326d214fd68e88 (diff) | |
- bug make_module_marker (plus de # et de .obj maintenant)
- portage (partiel) de Zarith
- bug discrEverywhere (manquait un "fun gls ->")
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@353 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Zarith/auxiliary.v | 1 | ||||
| -rw-r--r-- | theories/Zarith/zarith_aux.v | 14 |
2 files changed, 7 insertions, 8 deletions
diff --git a/theories/Zarith/auxiliary.v b/theories/Zarith/auxiliary.v index 9421573bd3..647f027c0c 100644 --- a/theories/Zarith/auxiliary.v +++ b/theories/Zarith/auxiliary.v @@ -8,7 +8,6 @@ (* $Id$ *) -Require Equality. Require Export Arith. Require fast_integer. Require zarith_aux. diff --git a/theories/Zarith/zarith_aux.v b/theories/Zarith/zarith_aux.v index 516bcb02ef..8b8be64acb 100644 --- a/theories/Zarith/zarith_aux.v +++ b/theories/Zarith/zarith_aux.v @@ -12,7 +12,7 @@ Require Arith. Require Export fast_integer. Tactic Definition ElimCompare [$com1 $com2] := - [<:tactic:< + [ < : tactic : < Elim (Dcompare (Zcompare $com1 $com2)); [ Idtac | Intro hidden_auxiliary; Elim hidden_auxiliary; @@ -90,7 +90,7 @@ Theorem Zgt_n_S : (n,m:Z)(Zgt m n) -> (Zgt (Zs m) (Zs n)). Unfold Zgt; Intros n m H; Rewrite Zcompare_n_S; Auto with arith. Save. -Lemma Zle_not_gt : (n,m:Z)(Zle n m)->~(Zgt n m). +Lemma Zle_not_gt : (n,m:Z)(Zle n m) -> ~(Zgt n m). Unfold Zle Zgt; Auto with arith. Save. @@ -101,13 +101,13 @@ Unfold Zgt ;Intros n; Elim (Zcompare_EGAL n n); Intros H1 H2; Rewrite H2; [ Discriminate | Trivial with arith ]. Save. -Lemma Zgt_not_sym : (n,m:Z)(Zgt n m)->~(Zgt m n). +Lemma Zgt_not_sym : (n,m:Z)(Zgt n m) -> ~(Zgt m n). Unfold Zgt ;Intros n m H; Elim (Zcompare_ANTISYM n m); Intros H1 H2; Rewrite -> H1; [ Discriminate | Assumption ]. Save. -Lemma Zgt_not_le : (n,m:Z)(Zgt n m)->~(Zle n m). +Lemma Zgt_not_le : (n,m:Z)(Zgt n m) -> ~(Zle n m). Unfold Zgt Zle not; Auto with arith. Save. @@ -446,18 +446,18 @@ Unfold Zle Zlt ;Intros n m; ElimCompare n m; [ | Elim (Zcompare_ANTISYM n m); Auto with arith ]. Save. -Theorem Zle_not_lt : (n,m:Z)(Zle n m)->~(Zlt m n). +Theorem Zle_not_lt : (n,m:Z)(Zle n m) -> ~(Zlt m n). Unfold Zle Zlt; Unfold not ;Intros n m H1 H2;Apply H1; Elim (Zcompare_ANTISYM n m);Auto with arith. Save. -Theorem Zlt_not_le : (n,m:Z)(Zlt n m)->~(Zle m n). +Theorem Zlt_not_le : (n,m:Z)(Zlt n m) -> ~(Zle m n). Unfold Zlt Zle not ;Intros n m H1 H2; Apply H2; Elim (Zcompare_ANTISYM m n); Auto with arith. Save. -Theorem Zlt_not_sym : (n,m:Z)(Zlt n m)->~(Zlt m n). +Theorem Zlt_not_sym : (n,m:Z)(Zlt n m) -> ~(Zlt m n). Intros n m H;Apply Zle_not_lt; Apply Zlt_le_weak; Assumption. Save. |