proposition: Lemma foldlE x r : foldl *%M x r = \big[*%M/1]_(y <- x :: r) y.
proof: Proof. by rewrite -foldrE; elim: r => [|y r IHr]/= in x *; rewrite ?mulm1 ?mulmA ?IHr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)