blob: 37b8bd44311bbf4d4b08065499f2cc1850299377 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
Require Import Coq.ZArith.ZArith.
Require Import Coq.ZArith.Znumtheory.
Require Import Coq.micromega.Lia.
Local Open Scope Z_scope.
Module Z.
Lemma prime_odd_or_2 : forall p (prime_p : prime p), p = 2 \/ Z.odd p = true.
Proof.
intros p prime_p.
apply Decidable.imp_not_l; try apply Z.eq_decidable.
intros p_neq2.
pose proof (Zmod_odd p) as mod_odd.
destruct (Sumbool.sumbool_of_bool (Z.odd p)) as [? | p_not_odd]; auto.
rewrite p_not_odd in mod_odd.
apply Zmod_divides in mod_odd; try omega.
destruct mod_odd as [c c_id].
rewrite Z.mul_comm in c_id.
apply Zdivide_intro in c_id.
apply prime_divisors in c_id; auto.
destruct c_id; [omega | destruct H; [omega | destruct H; auto] ].
pose proof (prime_ge_2 p prime_p); omega.
Qed.
Lemma odd_mod : forall a b, (b <> 0)%Z ->
Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a.
Proof.
intros a b H.
rewrite Zmod_eq_full by assumption.
rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul.
case_eq (Z.odd b); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r.
Qed.
End Z.
|
