proposition: Lemma Zdiv2_div : forall a, Z.div2 a = a/2.
proof: Proof. Proof Z.div2_div. Lemma Zmod_odd : forall a, a mod 2 = if Z.odd a then 1 else 0. Proof. intros a. now rewrite <- Z.bit0_odd, <- Z.bit0_mod. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms