diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-03-02 18:06:18 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-02 18:06:18 +0000 |
commit | c2ba535604cef5bc86369512e6f3c2833753a55a (patch) | |
tree | fd0b83022443a3806a5bac4e82299c513f5d2f8d /src/common/ZExtra.v | |
parent | 88d015ba178665ee21b282f364ccf047522e3b1c (diff) | |
download | vericert-c2ba535604cef5bc86369512e6f3c2833753a55a.tar.gz vericert-c2ba535604cef5bc86369512e6f3c2833753a55a.zip |
Update Coq version to 8.14.1
Diffstat (limited to 'src/common/ZExtra.v')
-rw-r--r-- | src/common/ZExtra.v | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/src/common/ZExtra.v b/src/common/ZExtra.v index 62ca54d..3a27cc6 100644 --- a/src/common/ZExtra.v +++ b/src/common/ZExtra.v @@ -45,12 +45,6 @@ Proof. - apply Z.mod_divide; assumption. Qed. -Lemma mod_0_r: forall (m: Z), - m mod 0 = 0. -Proof. - intros. destruct m; reflexivity. -Qed. - Lemma sub_mod_0: forall (a b m: Z), a mod m = 0 -> b mod m = 0 -> @@ -89,18 +83,6 @@ Proof. reflexivity. Qed. -Lemma mod_pow2_same_cases: forall a n, - a mod 2 ^ n = a -> - 2 ^ n = 0 /\ a = 0 \/ 0 <= a < 2 ^ n. -Proof. - intros. - assert (n < 0 \/ 0 <= n) as C by lia. destruct C as [C | C]. - - left. rewrite (Z.pow_neg_r 2 n C) in *. rewrite mod_0_r in H. auto. - - right. - rewrite <- H. apply Z.mod_pos_bound. - apply Z.pow_pos_nonneg; lia. -Qed. - Lemma mod_pow2_same_bounds: forall a n, a mod 2 ^ n = a -> 0 <= n -> |