proposition: Lemma Zsplit2 n : {p : Z * Z | let (x1, x2) := p in n = x1 + x2 /\ (x1 = x2 \/ x2 = x1 + 1)}.
proof: Proof. destruct (Z_modulo_2 n) as [(y,Hy)|(y,Hy)]; rewrite <- Z.add_diag in Hy. - exists (y, y). split. + assumption. + now left. - exists (y, y + 1). split. + now rewrite Z.add_assoc. + now right. Qed.
imports: BinInt