diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-08-04 13:07:16 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-08-04 13:07:16 -0400 |
| commit | d6770f633286d3292ad3a700c9af89e2704901d0 (patch) | |
| tree | 3ee75fa83e238156c11b4cb910a3e67c20b04aa3 /src/Util/NumTheoryUtil.v | |
| parent | 391fd7661eb7a48cd436c2375a4fa99978ebecd3 (diff) | |
address code review comments
Diffstat (limited to 'src/Util/NumTheoryUtil.v')
| -rw-r--r-- | src/Util/NumTheoryUtil.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index 8b8595bb7..f89eb6996 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -298,3 +298,10 @@ Proof. + prime_bound. + apply minus1_even_pow; [apply divide2_1mod4 | | apply Z_div_pos]; prime_bound. Qed. + + +Lemma odd_as_div a : Z.odd a = true -> a = (2*(a/2) + 1)%Z. +Proof. + rewrite Zodd_mod, <-Zeq_is_eq_bool; intro H_1; rewrite <-H_1. + apply Z_div_mod_eq; reflexivity. +Qed.
\ No newline at end of file |