proposition: Lemma add_mulE n m s : add_mul n m s = addn (muln n m) s.
proof: Proof. by elim: n => //= n IHn in m s *; rewrite IHn addE addnCA addnA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring