diff options
| author |  Raphaël Monat <raphael.monat@ens-lyon.org> | 2017-10-12 13:45:19 +0200 |
|---|---|---|
| committer | Raphaël Monat <raphael.monat@ens-lyon.org> | 2017-10-12 13:45:19 +0200 |
| commit | e5b43dcd5f449ccbc84c32868f9a9f6c3b73b263 (patch) | |
| tree | 5582c6e8aac9fd19806258d1eb2001f0e0cce20e /theories | |
| parent | 0a65d234346a73c98a9f65d2248edbbbe5e9fccb (diff) | |
Added proofs of Qeq_bool_refl, Qeq_bool_sym, Qeq_bool_trans.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/QArith/QArith_base.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index a94435c3f..121527c63 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -176,6 +176,21 @@ Proof. apply eq_true_iff_eq. rewrite !Qeq_bool_iff. now symmetry. Qed. +Lemma Qeq_bool_refl x: is_true (Qeq_bool x x). +Proof. + unfold is_true. rewrite Qeq_bool_iff. now reflexivity. +Qed. + +Lemma Qeq_bool_sym x y: is_true (Qeq_bool x y) -> is_true (Qeq_bool y x). +Proof. + unfold is_true. rewrite !Qeq_bool_iff. now symmetry. +Qed. + +Lemma Qeq_bool_trans x y z: is_true (Qeq_bool x y) -> is_true (Qeq_bool y z) -> is_true (Qeq_bool x z). +Proof. + unfold is_true. rewrite !Qeq_bool_iff. apply Qeq_trans. +Qed. + Hint Resolve Qnot_eq_sym : qarith. (** * Addition, multiplication and opposite *) |