diff options
| author |  Raphaël Monat <raphael.monat@ens-lyon.org> | 2017-10-08 21:27:14 +0200 |
|---|---|---|
| committer | Raphaël Monat <raphael.monat@ens-lyon.org> | 2017-10-08 21:27:14 +0200 |
| commit | 0a65d234346a73c98a9f65d2248edbbbe5e9fccb (patch) | |
| tree | 137e71100110b2be76a6a6924689514050285fbc /theories | |
| parent | 2ac3427a8366c28be37b33deb47e7823378263a3 (diff) | |
Changed Qeq_bool_sym into Qeq_bool_comm, used the proof of @letouzey.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/QArith/QArith_base.v | 14 |
1 files changed, 3 insertions, 11 deletions
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 16963b021..a94435c3f 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -171,17 +171,9 @@ Proof. auto with qarith. Qed. -Lemma Qeq_bool_sym x y: Qeq_bool x y = Qeq_bool y x. -Proof. - case_eq (Qeq_bool x y); intros H_eq_xy. - - unfold Qeq_bool in *. - rewrite <- Zeq_is_eq_bool in H_eq_xy. - rewrite H_eq_xy; symmetry. - rewrite <- Zeq_is_eq_bool; auto. - - apply Zeq_bool_neq in H_eq_xy. - case_eq (Qeq_bool y x); intros H_eq_yx. - + apply Zeq_is_eq_bool in H_eq_yx; congruence. - + auto. +Lemma Qeq_bool_comm x y: Qeq_bool x y = Qeq_bool y x. +Proof. + apply eq_true_iff_eq. rewrite !Qeq_bool_iff. now symmetry. Qed. Hint Resolve Qnot_eq_sym : qarith. |