proposition: Lemma mul_succ x y: T1nf x -> x * (T1succ y) = x * y + x.
proof: Proof. by move => h; rewrite succ_is_add_one mul_distr T1muln1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)