proposition: Lemma CompactGraph_b_correct2 : forall plFEX p s, inCompact p (CompactGraph_b plFEX s) -> inCompact (Cfst p) s.
proof: Proof. intros plFEX p s H e1 e2. simpl. unfold Cfst_raw. apply FinSubset_ball_closed. intros d dpos. set (d':=((1#2)*exist _ _ dpos)%Qpos). assert (Qeq (proj1_sig e1 + proj1_sig e2 + d) (proj1_sig ((e1 + d') + (d'+ e2))%Qpos)) by (simpl; ring). apply (@FinSubset_ball_wd_full _ _ _ H0 _ _ (reflexivity _) _ _ (reflexivity _)). clear H0. assert (H':=H e1 d'). clear H. unfold XY in *. destruct (approximate p e1) as [a b]. simpl in *. unfold Cjoin_raw in H'. simpl in *. unfold FinEnum_map_modulus, graphPoint_modulus in H'. remember (match mu f ((1#2)*d') with | Qpos2QposInf d => Qpos_min ((1#2)*d') d | QposInfinity => ((1#2)*d')%Qpos end) as d2. simpl in Heqd2. rewrite <- Heqd2 in H'. eapply FinSubset_ball_triangle_r with (approximate s d2). clear - H'. induction (approximate s d2). exfalso; exact (FinSubset_ball_nil H'). apply FinSubset_ball_orC in H'. destruct H' as [G | [H' _] | H'] using orC_ind. intro abs; contradict G; intro G; contradiction. intro abs; contradict abs. exists a0. split. left. reflexivity. assumption. apply FinSubset_ball_cons. apply IHl. assumption. eapply ball_weak_le;[|apply regFun_prf]. rewrite Heqd2. destruct (@mu X (Complete Y) f (Qpos_mult (@exist Q (Qlt {| Qnum := Z0; Qden := xH |}) {| Qnum := Z.pos xH; Qden := xO xH |} (@eq_refl comparison Lt)) d')) as [d0|]. simpl. assert (Qmin ((1#2)* proj1_sig d') (proj1_sig d0) <= ((1#2)*proj1_sig d')) by auto with *. apply Qplus_le_l. rewrite Q_Qpos_min. apply (Qle_trans _ _ _ H). apply Qmult_le_l. reflexivity. simpl. rewrite <- (Qmult_1_l d) at 2. apply Qmult_le_r. apply dpos. discriminate. simpl. apply Qplus_le_l. rewrite <- (Qmult_1_l ((1 # 2) * d)) at 2. apply Qmult_le_r. apply (Qpos_ispos d'). discriminate. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.metric2.Compact CoRN.metric2.Prelength CoRN.metric2.CompleteProduct CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax CoRN.logic.Classic