proposition: Lemma Rbar_plus'_comm : forall x y, Rbar_plus' x y = Rbar_plus' y x.
proof: Proof. intros [x| |] [y| |] ; try reflexivity. apply (f_equal (fun x => Some (Finite x))), Rplus_comm. Qed.
imports: Coq(Reals ssreflect) Rcomplements