proposition: Lemma NUMSUM_surjective n : exists b x, n = NUMSUM b x.
proof: Proof. exists (NUMLEFT n). exists (NUMRIGHT n). unfold NUMSUM, NUMLEFT, NUMRIGHT, NUMERAL, BIT1, BIT0. case_eq (even n); intro h. rewrite COND_False. rewrite even_spec in h. destruct h as [k h]. subst n. rewrite DIV_MULT. reflexivity. lia. rewrite COND_True. apply eq_false_negb_true in h. change (odd n = true) in h. rewrite odd_spec in h. destruct h as [k h]. subst. rewrite plus_1_minus_1. rewrite DIV_MULT. lia. lia. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat