proposition: Lemma mulnBl : left_distributive muln subn.
proof: Proof. move=> m n [|p]; first by rewrite !muln0. by elim: m n => // [m IHm] [|n] //; rewrite mulSn subnDl -IHm. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring