From 9412c0cc838f736fc5d5bea12b027048868a48fb Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 2 Jul 2020 02:34:28 +0100 Subject: Remove all <> Admitted --- src/common/ZExtra.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'src/common/ZExtra.v') diff --git a/src/common/ZExtra.v b/src/common/ZExtra.v index a0dd717..519ee7c 100644 --- a/src/common/ZExtra.v +++ b/src/common/ZExtra.v @@ -31,4 +31,19 @@ Module ZExtra. apply Zmult_gt_reg_r in g; lia. Qed. + Lemma Ple_not_eq : + forall x y, + (x < y)%positive -> x <> y. + Proof. lia. Qed. + + Lemma Pge_not_eq : + forall x y, + (y < x)%positive -> x <> y. + Proof. lia. Qed. + + Lemma Ple_Plt_Succ : + forall x y n, + (x <= y)%positive -> (x < y + n)%positive. + Proof. lia. Qed. + End ZExtra. -- cgit