proposition: Lemma sum_n_m_plus : forall (u v : nat -> G) (n m : nat), sum_n_m (fun k => plus (u k) (v k)) n m = plus (sum_n_m u n m) (sum_n_m v n m).
proof: Proof. intros u v n m. case: (le_dec n m) => Hnm. elim: m n u v Hnm => [ | m IH] ; case => [ | n] u v Hnm. by rewrite !sum_n_n. by apply Nat.nle_succ_0 in Hnm. rewrite !sum_n_Sm ; try by apply Nat.le_0_l. rewrite IH. rewrite -2!plus_assoc. apply f_equal. rewrite plus_comm -plus_assoc. apply f_equal, plus_comm. by apply Nat.le_0_l. rewrite /sum_n_m -!iter_nat_S -!/(sum_n_m _ n m). apply IH. by apply le_S_n. apply not_le in Hnm. rewrite !sum_n_m_zero //. by rewrite plus_zero_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub