proposition: Lemma sum_expr_S m l : (\sum_(i < l.+1) m ^ i = 1 + m * \sum_(i < l) m ^ i)%nat.
proof: Proof. rewrite big_ord_recl/= expn0 big_distrr/=; congr (_ + _)%N. by apply: eq_bigr => i _ /=; rewrite -expnS. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist