proposition: Lemma abs_pow_n : forall (x : K) n, abs (pow_n x n) <= (abs x)^n.
proof: Proof. induction n. apply Req_le, abs_one. simpl. apply: Rle_trans (abs_mult _ _) _. apply Rmult_le_compat_l with (2 := IHn). apply abs_ge_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub