proposition: Lemma mulA: associative T1mul.
proof: Proof. move => x y z; elim: z y x; first by move => a b; rewrite !T1muln0. move => a _ n b Hb; case; first by move => x; rewrite T1muln0 T1mul0n. move => a' n' b';case; [by rewrite !T1mul0n | move => a'' n'' b'' /=]. have aux: (n'' * (n' * n + n' + n) + n'' + (n' * n + n' + n))%N = ((n'' * n' + n'' + n') * n + (n'' * n' + n'' + n') + n)%N. rewrite ! mulnDl ! mulnDr mulnA ! addnA; congr (_ + _ + _)%N. rewrite - ! addnA; congr addn;rewrite addnCA; congr addn. by rewrite addnA addnC. case pa: (a'==zero); first rewrite (eqP pa). case pb: (a''== zero); rewrite ?(eqP pb) !andTb /= ? pb ? andFb. case pc: (a==zero) => /=;[ by rewrite aux | by rewrite pc Hb /=]. case pc: (a==zero) => /=; rewrite pb andFb ? aux // pc Hb /= pb //. case pb: (a==zero); rewrite /= ? pa ! andbF T1add_eq0 pa !andbF !andFb //. by rewrite T1addA Hb /= pa andbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)