proposition: Fact prime_2_or_odd p : prime p -> p = 2 \/ exists n, 0 < n /\ p = 2*n+1.
proof: Proof. intros Hp. assert (H1 : p <> 0). { generalize (prime_ge_2 Hp); lia. } assert (H3 : 2 <> 0) by discriminate. destruct (eq_nat_dec p 2) as [ | H2 ]; auto; right. assert (rem p 2 = 1) as Hp1. { generalize (div_rem_spec2 p H3). case_eq (rem p 2). + intros H _. apply divides_rem_eq in H. apply proj2 in Hp. destruct (Hp _ H); subst; lia. + intros; lia. } exists (div p 2); split. + generalize (div_rem_spec1 p 2) (prime_ge_2 Hp). destruct (div p 2); intros; lia. + rewrite Nat.mul_comm. rewrite (div_rem_spec1 p 2) at 1. f_equal; auto. Qed.
imports: Arith ZArith Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime php utils_nat) Undecidability.H10.ArithLibs(Zp)