proposition: Lemma sum3E n (f : nat -> nat) : \sum_(i < 3 * n) f i = \sum_(i < n) (f (3 * i) + f (3 * i).+1 + f (3 * i).+2).
proof: Proof. elim: n => [|n IH]; first by rewrite !big_ord0. by rewrite mulnS !big_ord_recr /= IH !addnA. Qed.
imports: mathcomp(all_ssreflect finmap)