proposition: Lemma plus_reg_l : forall r x y : G, plus r x = plus r y -> x = y.
proof: Proof. intros r x y H. rewrite -(plus_zero_l x) -(plus_opp_l r) -plus_assoc. rewrite H. now rewrite plus_assoc plus_opp_l plus_zero_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub