proposition: Lemma osum_of_nat n X: natp n -> (forall i, i <c n -> natp (X i)) -> osumf X n = csumb n X.
proof: Proof. move: n; apply: Nat_induction. by move => _; rewrite osum_f0 /csumb csum_trivial //; aw. move => m mN Hrec zp; rewrite (osum_fS _ mN) (succ_of_nat mN). have ha: forall i, i <c m -> natp (X i). move => i lim; apply: zp; exact: (clt_ltT lim (cltS mN)). have zmN:= (zp _ (cltS mN)); move: (Nat_decent mN) => mm. have sN: natp (csumb m X). apply:finite_sum_finite; split. by hnf; aw;move => i lim; rewrite LgV//; apply: ha; apply /(NltP mN). by aw; apply: finite_set_nat. by rewrite (csumA_setU1 X mm) (Hrec ha) csumC (osum2_2int zmN sN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)