proposition: Lemma size_sum_big s : s != [::] -> (size_sum s).+1 = (\sum_(k <- s) k.+1)%N.
proof: Proof. by case: s=> // a l _; rewrite size_sum_big_cons. 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