proposition: Lemma BishopCompact_Compact_BishopCompact1 : forall (P:Complete X->Prop) (HP:CompactSubset _ P) x, P x -> inCompact x (BishopCompactAsCompact HP).
proof: Proof. intros P [HP1 HP2 HP3] x Hx e1 e2. unfold BishopCompactAsCompact, approximate, BishopCompactAsCompact_raw, totallyBoundedSubset. destruct (HP2 ((1 # 2) * e2)%Qpos) as [l Hl0 Hl1]. destruct (Hl1 x Hx) as [y [Hy0 Hy1]]. clear - Hy0 Hy1. induction l. contradiction. destruct Hy0 as [Hy0|Hy0]. rewrite Hy0. intro abs; contradict abs. exists (approximate y ((1 # 2) * e2)%Qpos). split. left. reflexivity. rewrite <- ball_Cunit. assert (QposEq (e1+e2) (e1 + ((1 # 2) * e2 + (1 # 2) * e2))) by (unfold QposEq; simpl; ring). unfold QposEq in H. rewrite H. clear H. apply ball_triangle with x. apply ball_approx_l. apply ball_triangle with y. assumption. apply ball_approx_r. apply FinSubset_ball_cons. apply IHl. auto with *. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Limit CoRN.metric2.FinEnum Coq.ZArith.Zpow_facts CoRN.metric2.Complete CoRN.logic.Classic Coq.QArith.Qpower Coq.QArith.Qround