diff options
Diffstat (limited to 'theories/Reals/Cauchy/ConstructiveRcomplete.v')
| -rw-r--r-- | theories/Reals/Cauchy/ConstructiveRcomplete.v | 26 |
1 files changed, 5 insertions, 21 deletions
diff --git a/theories/Reals/Cauchy/ConstructiveRcomplete.v b/theories/Reals/Cauchy/ConstructiveRcomplete.v index 38eb9df0ea..c2b60e6478 100644 --- a/theories/Reals/Cauchy/ConstructiveRcomplete.v +++ b/theories/Reals/Cauchy/ConstructiveRcomplete.v @@ -690,20 +690,6 @@ Proof. exists x. exact c. Qed. -(* ToDO: Belongs into sumbool.v *) -Section connectives. - - Variables A B : Prop. - - Hypothesis H1 : {A} + {~A}. - Hypothesis H2 : {B} + {~B}. - - Definition sumbool_or_not_or : {A \/ B} + {~(A \/ B)}. - case H1; case H2; tauto. - Defined. - -End connectives. - Lemma Qnot_le_iff_lt: forall x y : Q, ~ (x <= y)%Q <-> (y < x)%Q. Proof. @@ -740,13 +726,11 @@ Proof. clear maj. right. exists n. apply H0. - clear H0 H. intro n. - apply sumbool_or_not_or. - + destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq b n - seq a n)%Q). - * left; assumption. - * right; apply Qle_not_lt; assumption. - + destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq d n - seq c n)%Q). - * left; assumption. - * right; apply Qle_not_lt; assumption. + 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. Definition CRealConstructive : ConstructiveReals |