diff options
| author |  Jade Philipoom <jadep@google.com> | 2018-02-16 18:15:18 +0100 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-02-23 13:06:33 -0500 |
| commit | 636ba579315b8f1fadf3714097d61378e3eff528 (patch) | |
| tree | fd8b52e7df121ff7ba08ac8ed898dec8dcc24d55 /src/Util/ZUtil | |
| parent | b54acb5b7012a8e4540e29c68d6f10f32b88009f (diff) | |
add three proofs to ZUtil
Diffstat (limited to 'src/Util/ZUtil')
| -rw-r--r-- | src/Util/ZUtil/Modulo.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v index d402055dd..e0a80544d 100644 --- a/src/Util/ZUtil/Modulo.v +++ b/src/Util/ZUtil/Modulo.v @@ -222,6 +222,9 @@ Module Z. : 0 <= c -> (a / b) mod c = a mod (c * b) / b. Proof. rewrite mod_pull_div_full; destruct (c <? 0) eqn:?; Z.ltb_to_lt; simpl; omega. Qed. + Lemma small_mod_eq a b n: a mod n = b mod n -> 0 <= a < n -> a = b mod n. + Proof. intros; rewrite <-(Z.mod_small a n); auto. Qed. + Lemma mod_pow_full p q n : (p^q) mod n = ((p mod n)^q) mod n. Proof. destruct (Z_dec' n 0) as [ [H|H] | H]; subst; |