diff options
| author | herbelin | 2003-11-12 19:19:56 +0000 |
|---|---|---|
| committer | herbelin | 2003-11-12 19:19:56 +0000 |
| commit | 634d52825790d8818883549616b3c8807655d2b8 (patch) | |
| tree | bef68618f7decd0f401931adc1f1043de3634c22 | |
| parent | ae8dadbbc2c96f50e80e952171396dd683b2d01f (diff) | |
Noms/énoncés plus canoniques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4875 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/ring/NArithRing.v | 6 | ||||
| -rw-r--r-- | theories/NArith/BinNat.v | 14 |
2 files changed, 10 insertions, 10 deletions
diff --git a/contrib/ring/NArithRing.v b/contrib/ring/NArithRing.v index 63483e5b1c..018503dc8a 100644 --- a/contrib/ring/NArithRing.v +++ b/contrib/ring/NArithRing.v @@ -30,13 +30,13 @@ Save. Definition NTheory : (Semi_Ring_Theory Nplus Nmult (Pos xH) Nul Neq). Split. Apply Nplus_comm. - Symmetry; Apply Nplus_assoc_l. + Symmetry; Apply Nplus_assoc. Apply Nmult_comm. - Symmetry; Apply Nmult_assoc_l. + Symmetry; Apply Nmult_assoc. Apply Nplus_0_l. Apply Nmult_1_l. Apply Nmult_0_l. - Apply Nmult_Nplus_distr_l. + Apply Nmult_plus_distr_r. Apply Nplus_reg_l. Apply Neq_prop. Save. diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 4d3d30f212..084afccbc0 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -106,7 +106,7 @@ NewDestruct n; NewDestruct m; Simpl; Try Reflexivity. Rewrite add_sym; Reflexivity. Qed. -Theorem Nplus_assoc_l : +Theorem Nplus_assoc : (n,m,p:entier)(Nplus (Nplus n m) p)=(Nplus n (Nplus m p)). Proof. Intros. @@ -162,7 +162,7 @@ NewDestruct n; NewDestruct m; Simpl; Try Reflexivity. Rewrite times_sym; Reflexivity. Qed. -Theorem Nmult_assoc_l : +Theorem Nmult_assoc : (n,m,p:entier)(Nmult (Nmult n m) p)=(Nmult n (Nmult m p)). Proof. Intros. @@ -172,7 +172,7 @@ NewDestruct p; Try Reflexivity. Simpl; Rewrite times_assoc; Reflexivity. Qed. -Theorem Nmult_Nplus_distr_l : +Theorem Nmult_plus_distr_r : (n,m,p:entier)(Nmult (Nplus n m) p)=(Nplus (Nmult n p) (Nmult m p)). Proof. Intros. @@ -181,11 +181,11 @@ NewDestruct m; NewDestruct p; Try Reflexivity. Simpl; Rewrite times_add_distr_l; Reflexivity. Qed. -Theorem Nmult_int_r : (n,m,p:entier) (Nmult n p)=(Nmult m p) -> n=m\/p=Nul. +Theorem Nmult_reg_r : (n,m,p:entier) ~p=Nul->(Nmult n p)=(Nmult m p) -> n=m. Proof. -NewDestruct p; Intro H. -Right; Reflexivity. -Left; NewDestruct n; NewDestruct m; Reflexivity Orelse Try Discriminate H. +NewDestruct p; Intros Hp H. +Contradiction Hp; Reflexivity. +NewDestruct n; NewDestruct m; Reflexivity Orelse Try Discriminate H. Injection H; Clear H; Intro H; Rewrite simpl_times_r with 1:=H; Reflexivity. Qed. |