proposition: Lemma abs_minus : forall x y : K, abs (minus x y) = abs (minus y x).
proof: Proof. intros x y. by rewrite /minus -abs_opp opp_plus opp_opp plus_comm. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub