proposition: Lemma nat_to_B_sum x y: nat_to_B (x + y) = nat_to_B x +c nat_to_B y.
proof: Proof. elim: y => [|n hrec /=]. rewrite addn0 csum0r //; exact (CS_nat (nat_to_B_Nat x)). by rewrite (csum_nS _ (nat_to_B_Nat n)) addnS - hrec. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)