proposition: Lemma CompactGraph_correct2 : forall plFEX p s, inCompact p (CompactGraph 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. pose proof (H e1 d') as H'. clear H. unfold XY in *. destruct (approximate p e1) as [a b]. simpl in *. unfold FinEnum_map_modulus, graphPoint_modulus in H'. set (d2:=match mu f d' with | Qpos2QposInf d => Qpos_min d' d | QposInfinity => d' end) in *. 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]. unfold d2. destruct (mu f d') as [d0|]; auto with *. simpl. rewrite Q_Qpos_min. assert (Qmin (proj1_sig d') (proj1_sig d0) <= proj1_sig d') by auto with *. apply Qplus_le_l. exact H. 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