proposition: Lemma CompactGraph_correct : forall plX plFEX x y s, inCompact (Couple (x,y)) (CompactGraph plFEX s) <-> (inCompact x s /\ msp_eq y (Cmap plX f x)).
proof: Proof. intros plX plFEX x y s. split; intros H. split; rewrite <- (CoupleCorrect2 x y). apply (@CompactGraph_correct2 plFEX). exact H. symmetry. transitivity (Csnd (Couple (x,y))). refine (CompactGraph_correct3 _ _). apply H. apply CoupleCorrect3. destruct H as [H0 H1]. change (x, y) with (PairMS x y). rewrite -> H1. apply CompactGraph_correct1. auto. 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