proposition: Lemma sum_rcons a l (F: nat -> nat): \sum_(i <- rcons l a) F i = F a + \sum_(i <- l) F i.
proof: Proof. by elim: l a => [a | a l Ih b]; rewrite /= !big_cons ?big_nil // Ih addnCA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)