proposition: Lemma Zdiv2_odd_eqn n : n = 2*(Z.div2 n) + if Z.odd n then 1 else 0.
proof: Proof. Proof (Z.div2_odd n). Lemma Zeven_div2 n : Zeven n -> n = 2 * Z.div2 n. Proof. boolify_even_odd. rewrite <- Z.negb_odd, Bool.negb_true_iff. intros Hn. rewrite (Zdiv2_odd_eqn n) at 1. now rewrite Hn, Z.add_0_r. Qed.
imports: BinInt