proposition: Lemma Rbar_plus_le_compat (a b c d : Rbar) : Rbar_le a b -> Rbar_le c d -> Rbar_le (Rbar_plus a c) (Rbar_plus b d).
proof: Proof. case: a => [a | | ] // ; case: b => [b | | ] // ; case: c => [c | | ] // ; case: d => [d | | ] //. apply Rplus_le_compat. intros _ _. apply Rle_refl. intros _ _. apply Rle_refl. Qed.
imports: Coq(Reals ssreflect) Rcomplements