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