proposition: Lemma nat_to_B_prod x y: nat_to_B (x * y) = nat_to_B x *c nat_to_B y.
proof: Proof. elim: y =>[| n hrec /=]; first by rewrite muln0 cprod0r. by rewrite (cprod_nS _ (nat_to_B_Nat n)) mulnS nat_to_B_sum hrec csumC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)