proposition: Lemma Z_modulo_2 n : {y | n = 2 * y} + {y | n = 2 * y + 1}.
proof: Proof. destruct (Zeven_odd_dec n) as [Hn|Hn]. - left. exists (Z.div2 n). exact (Zeven_div2 n Hn). - right. exists (Z.div2 n). exact (Zodd_div2 n Hn). Qed.
imports: BinInt