proposition: Lemma mysum_recl m n F : m <= n -> \mysum_(m <= i < n.+1) F i = \mysum_(m <= i < n) F i + F n.
proof: Proof. move=> leq_mn; rewrite /mysum subSn// -addn1 iotaD subnKC//= foldr_cat/=. elim: (iota _ _) (F n) => [|x s IHs] k /=; first by rewrite addn0. by rewrite IHs addnA. Qed.
imports: mathcomp(all_ssreflect)