diff options
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 |