proposition: Lemma T1log_prod a b: a != zero -> b != zero -> T1log(a * b) = T1log a + T1log b.
proof: Proof. case: a b => // a1 n1 b1;case => // a2 n2 b2 _ _. rewrite /=; case p1: (a1==zero); case p2: (a2==zero) => //=. by rewrite (eqP p1) (eqP p2). by rewrite (eqP p2) T1addn0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)