diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-02-26 20:01:18 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-02-26 20:17:45 +0100 |
| commit | 20adaabfa96744442f201287e2900b1575614577 (patch) | |
| tree | b6b3de973bcc250a653f8605032abc5ababfeecb /theories/QArith | |
| parent | ea05377f19404e0627a105b07c10ce72fb010af9 (diff) | |
Qcanon : fix names of lemmas Qcle_alt & Qcge_alt (were Qle_alt & Qge_alt)
Diffstat (limited to 'theories/QArith')
| -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. |