proposition: Lemma CompactCompleteCompact_correct : forall x s, inCompact x s <-> inCompact (Cjoin x) (CompactCompleteCompact s).
proof: Proof. intros x s. split. intros H e1 e2. simpl. unfold Cjoin_raw. simpl. assert (Z:=(H ((1#2)*e1) ((1#2)*e2))%Qpos). intro abs. unfold FinSubset_ball in Z. contradict Z; intros [z [Hz1 Hz0]]. revert abs. apply InFinEnumC_weaken in Hz1. rewrite -> FinCompact_correct in Hz1. apply FinSubset_ball_closed. intros d dpos. assert (Z0:=(Hz0 ((1#2)*e1) ((1#2)*exist _ _ dpos))%Qpos). assert (Z1:=(Hz1 ((1#2)*exist _ _ dpos) ((1#2)*e2))%Qpos). simpl in Z1. set (w0:=((1 # 2) * e1 + ((1 # 2) * e1 + (1 # 2) * e2) + (1 # 2) * exist _ _ dpos)%Qpos) in *. set (w1:= ((1 # 2) * exist _ _ dpos + (1 # 2) * e2)%Qpos) in *. assert (Qeq (proj1_sig e1 + proj1_sig e2 + d) (proj1_sig (w0 + w1)%Qpos)) by (unfold w0, w1; simpl; ring). apply (@FinSubset_ball_wd_full _ _ _ H0 _ _ (reflexivity _) _ _ (reflexivity _)). clear H0. eapply FinSubset_ball_triangle_l. apply Z0. apply Z1. intros H e1 e2. apply FinSubset_ball_closed. intros d dpos. set (d':=((1#4)*exist _ _ dpos)%Qpos). assert (Qeq (proj1_sig e1 + proj1_sig e2 + d) (proj1_sig ((e1 + (1#2)*d' + (1#2)*d') + (((d' + d') + (1#2)*d') + ((1#2)*d' + e2)))%Qpos)) by (unfold d'; simpl; ring). apply (@FinSubset_ball_wd_full _ _ _ H0 _ _ (reflexivity _) _ _ (reflexivity _)). clear H0. eapply FinSubset_ball_triangle_l. eapply ball_triangle. apply regFun_prf. apply ball_approx_r. eapply FinSubset_ball_triangle_r;[|apply regFun_prf]. assert (Z:= (H d' d')). simpl in Z. unfold Cjoin_raw in Z. intro abs. unfold FinSubset_ball in Z. contradict Z; intros [z [Hz1 Hz0]]. revert abs. apply InFinEnumC_weaken in Hz1. change (InFinEnumC (X:=X) z (approximate (FinCompact (approximate s ((1 # 2) * d')%Qpos)) ((1 # 2) * d')%Qpos)) in Hz1. apply FinSubset_ball_triangle_l with (Cunit z). rewrite -> ball_Cunit. assumption. clear - Hz1. induction ((approximate s ((1 # 2) * d')%Qpos)). exfalso; exact (FinSubset_ball_nil Hz1). apply FinSubset_ball_orC in Hz1. destruct Hz1 as [G | Hz1 | Hz1] using orC_ind. intro abs; contradict G; intro G; contradiction. intro abs; contradict abs. exists a. split. left. reflexivity. rewrite -> Hz1. apply ball_approx_l. apply FinSubset_ball_cons. apply IHm; auto. 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 CoRN.metric2.Prelength