proposition: Lemma base2r_zero: base_two_reverse \0c = \0c.
proof: Proof. rewrite / base_two_reverse (the_expansion_zero NS2 clt_12). by rewrite domain_set0 cardinal_set0; apply: csum_trivial; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)