diff options
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. |