proposition: Lemma opp_plus : forall x y : G, opp (plus x y) = plus (opp x) (opp y).
proof: Proof. intros x y. apply plus_reg_r with (plus x y). rewrite plus_opp_l. rewrite plus_assoc. rewrite (plus_comm (opp x)). rewrite <- (plus_assoc (opp y)). rewrite plus_opp_l. rewrite plus_zero_r. apply sym_eq, plus_opp_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub