diff options
| author | coq | 2001-04-20 16:00:43 +0000 |
|---|---|---|
| committer | coq | 2001-04-20 16:00:43 +0000 |
| commit | d857c99c6c985eb36ce8a4b2667dc0b5ccca115c (patch) | |
| tree | 2ea53c80dd3319b24c38b15cb5be5a582c9b302a /theories/IntMap/Addec.v | |
| parent | 4837b599b4f158decc91f615a25e3a636c6ced5d (diff) | |
Library doc adjustments (until page 140)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1655 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/IntMap/Addec.v')
| -rw-r--r-- | theories/IntMap/Addec.v | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/theories/IntMap/Addec.v b/theories/IntMap/Addec.v index abbe450816..72ad3d9866 100644 --- a/theories/IntMap/Addec.v +++ b/theories/IntMap/Addec.v @@ -73,7 +73,8 @@ Proof. Intros. Rewrite (ad_xor_eq a a' H). Apply ad_eq_correct. Qed. -Lemma ad_xor_eq_false : (a,a':ad) (p:positive) (ad_xor a a')=(ad_x p) -> (ad_eq a a')=false. +Lemma ad_xor_eq_false + : (a,a':ad) (p:positive) (ad_xor a a')=(ad_x p) -> (ad_eq a a')=false. Proof. Intros. Elim (sumbool_of_bool (ad_eq a a')). Intro H0. Rewrite (ad_eq_complete a a' H0) in H. Rewrite (ad_xor_nilpotent a') in H. Discriminate H. @@ -115,14 +116,16 @@ Proof. Intro H0. Rewrite ad_eq_comm. Assumption. Qed. -Lemma ad_bit_0_neq : (a,a':ad) (ad_bit_0 a)=false -> (ad_bit_0 a')=true -> (ad_eq a a')=false. +Lemma ad_bit_0_neq + : (a,a':ad) (ad_bit_0 a)=false -> (ad_bit_0 a')=true -> (ad_eq a a')=false. Proof. Intros. Elim (sumbool_of_bool (ad_eq a a')). Intro H1. Rewrite (ad_eq_complete ? ? H1) in H. Rewrite H in H0. Discriminate H0. Trivial. Qed. -Lemma ad_div_eq : (a,a':ad) (ad_eq a a')=true -> (ad_eq (ad_div_2 a) (ad_div_2 a'))=true. +Lemma ad_div_eq + : (a,a':ad) (ad_eq a a')=true -> (ad_eq (ad_div_2 a) (ad_div_2 a'))=true. Proof. Intros. Cut a=a'. Intros. Rewrite H0. Apply ad_eq_correct. Apply ad_eq_complete. Exact H. |