From d6770f633286d3292ad3a700c9af89e2704901d0 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 4 Aug 2016 13:07:16 -0400 Subject: address code review comments --- src/Util/NumTheoryUtil.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/Util/NumTheoryUtil.v') 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 -- cgit v1.2.3