proposition: Lemma odd_bound_1 : forall p i, p mod 2 = 1 -> i < Z.succ (p / 2) -> 2 * i < p.
proof: Proof. intros p i Op Bi. unfold Z.succ in Bi. apply Z.le_lt_trans with (2 * (p / 2)). lia. rewrite Z_mult_div_mod; [ | auto with * ]. rewrite Op; auto with *. Qed.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm Znumfacts