fact: Fixpoint size_sum_rec k (s : seq nat) : nat := if s is x :: l then (k + (size_sum_rec x l).+1)%N else k.
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