diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-07-02 02:34:28 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-02 02:34:28 +0100 |
| commit | 9412c0cc838f736fc5d5bea12b027048868a48fb (patch) | |
| tree | 512ac804502513525cde6f2731b991b6e1a20f78 /src/common | |
| parent | 89bc64204b4d99cb7dc9eacb1ecdf26b30dc26a0 (diff) | |
| download | vericert-9412c0cc838f736fc5d5bea12b027048868a48fb.tar.gz vericert-9412c0cc838f736fc5d5bea12b027048868a48fb.zip | |
Remove all <> Admitted
Diffstat (limited to 'src/common')
| -rw-r--r-- | src/common/ZExtra.v | 15 |
1 files changed, 15 insertions, 0 deletions
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. |