proposition: Lemma T1mul_eq1 a b: T1nf a -> (a* b == one) = ((a == one) && (b == one)).
proof: Proof. case: a => //; [ by rewrite T1mul0n | move => a' n' b']. case: b => //; [ by rewrite T1muln0 andbF | move => a n b]. simpl; case pa: (a'== zero); last first. case pb: (a==zero);rewrite !T1eqE pa // T1add_eq0 pa //. case pb: (a== zero); last by rewrite andbF !T1eqE (T1add_eq0) pb ! andbF. rewrite (eqP pa) T1lt1; move /and3P => [_ _ /eqP ->]. by rewrite /= !T1eqE pb /=; case n' => // m; case n => //=; rewrite muln0 addn0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)