proposition: Lemma pow_n_comm : forall (x : K) n m, mult (pow_n x n) (pow_n x m) = mult (pow_n x m) (pow_n x n).
proof: Proof. intros x n m. rewrite -2!pow_n_plus. by apply f_equal, Nat.add_comm. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub