proposition: Lemma Rplus_lt_epsilon : forall {R : ConstructiveReals} (a b c d : CRcarrier R), (a + b) < (c + d) -> sum (a < c) (b < d).
proof: Proof. intros. destruct (CRltLinear R). destruct (s (a+b) (a+d) (c+d) H). - right. apply CRplus_lt_reg_l in c0. exact c0. - left. apply CRplus_lt_reg_r in c0. exact c0. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal