proposition: Lemma size_sum_big_cons : forall s x, (size_sum (x :: s)).+1 = (\sum_(k <- x :: s) k.+1)%N.
proof: Proof. elim=> [s|n s IHn x] /=; rewrite big_cons. by rewrite big_nil addn0. by rewrite IHn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm poly mxpoly finfun tuple) mathcomp(matrix bigop zmodp polydiv) ssrcomplements dvdring