proposition: Lemma foldl_idx r : foldl *%M 1 r = \big[*%M/1]_(x <- r) x.
proof: Proof. by rewrite foldlE big_cons mul1m. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)