proposition: Lemma base2r_one: base_two_reverse \1c = \1c.
proof: Proof. rewrite / base_two_reverse (the_expansion_digit NS2 clt_12 card1_nz clt_12). move: (simple_fct2 \0c \1c) => [_ sb _ _ h]. rewrite sb cardinal_set1 /expansion_value Lgd csum_trivial3 h cpowx0. have zz: inc \0c (singleton \0c) by fprops. rewrite !LgV //; first by rewrite (cprod1r CS1) (card_card CS1). rewrite succ_zero cdiff_nn; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)