diff options
| author |  Raphaël Monat <raphael.monat@ens-lyon.org> | 2017-10-25 16:14:10 +0200 |
|---|---|---|
| committer | Raphaël Monat <raphael.monat@ens-lyon.org> | 2017-10-25 16:15:06 +0200 |
| commit | 5431b0f17cd73a09472093e779cc1508b3b3ac4f (patch) | |
| tree | d5a4d2af8d6872234b9cc8201afe5e520d9ab1e9 /theories | |
| parent | e5b43dcd5f449ccbc84c32868f9a9f6c3b73b263 (diff) | |
Moving from `is_true` to `= true`
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/QArith/QArith_base.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 121527c63..66740512b 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -176,19 +176,19 @@ Proof. apply eq_true_iff_eq. rewrite !Qeq_bool_iff. now symmetry. Qed. -Lemma Qeq_bool_refl x: is_true (Qeq_bool x x). +Lemma Qeq_bool_refl x: Qeq_bool x x = true. Proof. - unfold is_true. rewrite Qeq_bool_iff. now reflexivity. + 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). +Lemma Qeq_bool_sym x y: Qeq_bool x y = true -> Qeq_bool y x = true. Proof. - unfold is_true. rewrite !Qeq_bool_iff. now symmetry. + 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). +Lemma Qeq_bool_trans x y z: Qeq_bool x y = true -> Qeq_bool y z = true -> Qeq_bool x z = true. Proof. - unfold is_true. rewrite !Qeq_bool_iff. apply Qeq_trans. + rewrite !Qeq_bool_iff. apply Qeq_trans. Qed. Hint Resolve Qnot_eq_sym : qarith. |