proposition: Lemma Compact_BishopCompact_Compact : forall s, msp_eq s (BishopCompactAsCompact (CompactAsBishopCompact locatedX s)).
proof: Proof. intros s e1 e2. rewrite Qplus_0_r. assert (QposEq (e1 + e2) (e1 + (1#5)*((1#2)*e2) + ((3#5)*((1#2)*e2) + (1#2)*e2) + (1#10)*e2)) by (unfold QposEq; simpl; ring). unfold QposEq in H. rewrite H. clear H. apply ball_weak. apply Qpos_nonneg. apply ball_triangle with (approximate s ((1#5)*((1#2)*e2))%Qpos). apply regFun_prf. clear e1. rewrite -> FinEnum_map_Cunit. apply ball_triangle with (CompactTotalBound locatedX s ((1 # 2) * e2)). apply CompactTotalBoundNotFar. unfold ball, FinEnum. unfold BishopCompactAsCompact, approximate, BishopCompactAsCompact_raw. unfold totallyBoundedSubset, CompactAsBishopCompact, CompactTotallyBounded. change (FinEnum_ball (Complete X)) with (@ball (FinEnum (Complete X))). induction (CompactTotalBound locatedX s ((1 # 2) * e2)). apply ball_refl. apply Qpos_nonneg. destruct IHl as [_ [IHlA IHlB]]. split. apply Qpos_nonneg. split; intros x Hx; apply FinSubset_ball_orC in Hx; (destruct Hx as [G | Hx | Hx] using orC_ind; [auto using existsC_stable |apply existsWeaken |]). exists (Cunit (approximate a ((1 # 2) * e2)%Qpos)). split. intro abs; contradict abs. exists (Cunit (approximate a ((1 # 2) * e2)%Qpos)). split. left. reflexivity. reflexivity. rewrite -> Hx. apply ball_approx_r. destruct (IHlA x Hx) as [ G | y [Hy0 Hy1]] using existsC_ind. auto using existsC_stable. apply existsWeaken. exists y. split; auto. apply FinSubset_ball_cons. exact Hy0. exists a. split. intro abs; contradict abs. exists a. split. left. reflexivity. reflexivity. rewrite -> Hx. apply ball_approx_l. destruct (IHlB x Hx) as [ G | y [Hy0 Hy1]] using existsC_ind. auto using existsC_stable. apply existsWeaken. exists y. split; auto. apply FinSubset_ball_cons. exact Hy0. 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