diff options
| author |  Raphaël Monat <raphael.monat@ens-lyon.org> | 2017-10-03 16:19:37 +0200 |
|---|---|---|
| committer | Raphaël Monat <raphael.monat@ens-lyon.org> | 2017-10-03 16:19:37 +0200 |
| commit | d4009edb53ab7780bc85d83ccf01c6920c7f09e1 (patch) | |
| tree | e0c08409b7086ddcef4c54fc3bd3d00dc456b1b4 /theories | |
| parent | b40eb1628b85bbf4605fad2222c86ea796425e2a (diff) | |
Add Qeq_bool_sym: Qeq_bool x y = Qeq_bool y x.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/QArith/QArith_base.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index a19f9f902..16963b021 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -171,6 +171,19 @@ 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. +Qed. + Hint Resolve Qnot_eq_sym : qarith. (** * Addition, multiplication and opposite *) |