From 0a65d234346a73c98a9f65d2248edbbbe5e9fccb Mon Sep 17 00:00:00 2001 From: Raphaël Monat Date: Sun, 8 Oct 2017 21:27:14 +0200 Subject: Changed Qeq_bool_sym into Qeq_bool_comm, used the proof of @letouzey. --- theories/QArith/QArith_base.v | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) (limited to 'theories') 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. -- cgit v1.2.3