proposition: Lemma Rbar_plus_lt_compat (a b c d : Rbar) : Rbar_lt a b -> Rbar_lt c d -> Rbar_lt (Rbar_plus a c) (Rbar_plus b d).
proof: Proof. case: a => [a | | ] // ; case: b => [b | | ] // ; case: c => [c | | ] // ; case: d => [d | | ] // ; apply Rplus_lt_compat. Qed.
imports: Coq(Reals ssreflect) Rcomplements