proposition: Lemma pow_n_plus : forall (x : K) (n m : nat), pow_n x (n+m) = mult (pow_n x n) (pow_n x m).
proof: Proof. intros x. elim => /= [ | n IH] m. by rewrite mult_one_l. by rewrite IH mult_assoc. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub