proposition: Lemma T1muln1 x: T1nf x -> x * one = x.
proof: Proof. case: x => // a n b /= /and3P[_ _]; rewrite muln0 add0n addn0. by case (altP (a =P zero)) => // ->; rewrite T1lt1 eqxx => /eqP ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)