proposition: Lemma minus_trans (r x y : G) : minus x y = plus (minus x r) (minus r y).
proof: Proof. rewrite /minus -!plus_assoc. apply f_equal. by rewrite plus_assoc plus_opp_l plus_zero_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub