proposition: Lemma mul_int_limit n y: T1limit y -> \F n.+1 * y = y.
proof: Proof. elim y => // a _ m b Hb /=. case pa: (a==zero) => //;case pb: (b==zero); last by move/Hb => ->. by rewrite (eqP pb) T1muln0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)