proposition: Lemma Ndouble_or_double_plus_un a : {a0 : N | a = N.double a0} + {a1 : N | a = N.succ_double a1}.
proof: Proof. elim (sumbool_of_bool (N.odd a)); intros H; [right|left]; exists (N.div2 a); symmetry; rewrite ?N.succ_double_spec, ?N.double_spec, N.div2_odd, H, ?N.add_0_r; trivial. Qed.
imports: Bool Sumbool Arith BinPos BinNat Pnat Nnat Ndigits