proposition: Lemma sum_varP s : 0 \notin s -> sum_var s = variation (head 0 s) (last 0 s).
proof: Proof. rewrite /sum_var /variation. case: s => /= [_|a s]; first by rewrite big_nil sgz0 mul0r. rewrite in_cons big_cons mul0r ltxx mulr0 add0r. elim: s a => [|b s IHs] a; first by rewrite big_nil le_gtF ?mulr0 ?sqr_ge0. move=> /norP [neq_0a Hbs]; move: (Hbs); rewrite in_cons => /norP[neq_0b Hs]. rewrite /= big_cons IHs ?negb_or ?neq_0b // -!sgz_cp0 !sgzM. have: (last b s) != 0 by apply: contra Hbs => /eqP <-; rewrite mem_last. by move: neq_0a neq_0b; do 3?case: sgzP => ? //. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)