proposition: Lemma Zodd_quot2 n : n >= 0 -> Zodd n -> n = 2 * Z.quot2 n + 1.
proof: Proof. intros Hn Hn'. apply Zodd_bool_iff in Hn'. rewrite (Zquot2_odd_eqn n) at 1. rewrite Hn'. f_equal. destruct n; (now destruct Hn) || easy. Qed.
imports: BinInt