diff options
| -rw-r--r-- | theories/QArith/Qcanon.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 86be28d7b..078926e32 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -130,12 +130,12 @@ Proof. intros; exact (Qgt_alt p q). Qed. -Lemma Qle_alt : forall p q, (p<=q) <-> (p?=q <> Gt). +Lemma Qcle_alt : forall p q, (p<=q) <-> (p?=q <> Gt). Proof. intros; exact (Qle_alt p q). Qed. -Lemma Qge_alt : forall p q, (p>=q) <-> (p?=q <> Lt). +Lemma Qcge_alt : forall p q, (p>=q) <-> (p?=q <> Lt). Proof. intros; exact (Qge_alt p q). Qed. |