proposition: Lemma sum_inequa_Rle_lt_depr : forall a x b c y d:R, a <= x -> x < b -> c < y -> y <= d -> a + c < x + y < b + d.
proof: Proof. intros; split. - apply Rlt_le_trans with (a + y); auto with real. - apply Rlt_le_trans with (b + y); auto with real. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField