proposition: Lemma sum_n_switch : forall (u : nat -> nat -> G) (m n : nat), sum_n (fun i => sum_n (u i) n) m = sum_n (fun j => sum_n (fun i => u i j) m) n.
proof: Proof. intros u. rewrite /sum_n. induction m ; simpl ; intros n. rewrite sum_n_n. apply iter_nat_ext_loc => k Hk. rewrite sum_n_n. by []. rewrite !sum_n_Sm. rewrite IHm ; clear IHm. rewrite -sum_n_m_plus. apply sum_n_m_ext_loc => k Hk. rewrite sum_n_Sm //. by apply Nat.le_0_l. by apply Nat.le_0_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub