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