proposition: Lemma b_timesm n m: beautiful n -> beautiful (m * n).
proof: Proof. elim:m=>[_|m Hm Bn]; first by rewrite mul0n; apply: b_0. move: (Hm Bn)=> H1. by rewrite mulSn; apply: (b_sum _ n (m * n))=>//. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq)