proposition: Lemma CRealLtDisjunctEpsilon : forall a b c d : CReal, (CRealLtProp a b \/ CRealLtProp c d) -> CRealLt a b + CRealLt c d.
proof: Proof. intros. assert (exists n : Z, 2*2^n < seq b n - seq a n \/ 2*2^n < seq d n - seq c n)%Q. { destruct H. - destruct H as [n maj]. exists n. left. apply maj. - destruct H as [n maj]. exists n. right. apply maj. } apply constructive_indefinite_ground_description_Z in H0. - destruct H0 as [n maj]. destruct (Qlt_le_dec (2 * 2^n) (seq b n - seq a n)). + left. exists n. apply q. + assert (2 * 2^n < seq d n - seq c n)%Q. { destruct maj. - exfalso. apply (Qlt_not_le (2 * 2^n) (seq b n - seq a n)); assumption. - assumption. } clear maj. right. exists n. apply H0. - clear H0 H. intro n. destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq b n - seq a n)%Q) as [H1|H1]. + now left; left. + destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq d n - seq c n)%Q) as [H2|H2]. * now left; right. * now right; intros [H3|H3]; apply Qle_not_lt with (2 := H3). Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra Qminmax