diff options
Diffstat (limited to 'theories/IntMap/Addec.v')
| -rw-r--r-- | theories/IntMap/Addec.v | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/theories/IntMap/Addec.v b/theories/IntMap/Addec.v index 72ad3d9866..64c5337288 100644 --- a/theories/IntMap/Addec.v +++ b/theories/IntMap/Addec.v @@ -73,8 +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. @@ -116,22 +116,23 @@ 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. Qed. -Lemma ad_div_neq : (a,a':ad) (ad_eq (ad_div_2 a) (ad_div_2 a'))=false -> (ad_eq a a')=false. +Lemma ad_div_neq : (a,a':ad) (ad_eq (ad_div_2 a) (ad_div_2 a'))=false -> + (ad_eq a a')=false. Proof. Intros. Elim (sumbool_of_bool (ad_eq a a')). Intro H0. Rewrite (ad_eq_complete ? ? H0) in H. Rewrite (ad_eq_correct (ad_div_2 a')) in H. Discriminate H. |