diff options
Diffstat (limited to 'theories/NArith/BinPos.v')
| -rw-r--r-- | theories/NArith/BinPos.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index 0a1cd9ab4..20cfb43a3 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -751,6 +751,13 @@ Proof. destruct (Pcompare_not_Eq p q) as (_,H'); elim H'; auto. Qed. +Lemma Pcompare_eq_iff : forall p q:positive, (p ?= q) Eq = Eq <-> p = q. +Proof. + split. + apply Pcompare_Eq_eq. + intros; subst; apply Pcompare_refl. +Qed. + Lemma Pcompare_Gt_Lt : forall p q:positive, (p ?= q) Gt = Lt -> (p ?= q) Eq = Lt. Proof. |