proposition: Lemma NUMLEFT_NUMSUM b n : NUMLEFT (NUMSUM b n) = b.
proof: Proof. unfold NUMSUM, NUMERAL, BIT1, BIT0, NUMLEFT. destruct (prop_degen b); subst. rewrite COND_True, even_succ, odd_mul, odd_2. reflexivity. rewrite COND_False, even_double. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat