proposition: Lemma IFE_gleP x y: gle IFS_order x y <-> [/\ inc x IFSE, inc y IFSE & [\/ P (P x) <c P (P y), P (P x) = P (P y) /\ Q x <q Q y | [/\ P (P x) = P (P y), Q x = Q y & Q (P x) <=c Q (P y)]]].
proof: Proof. split. move => /graph_on_P1 [xe ye h]; split => //. case: h. move ->; constructor 3; split => //; apply: cleR. by move/Zo_S: ye => /setX_P [_ /setX_P [_ _ /CS_nat rc] _]. case. by constructor 1. by constructor 2. by move =>[ra rb /proj1 rc]; constructor 3. move =>[xe ye h]; apply/graph_on_P1; split => //. case: (equal_or_not x y ) => eab; [ by left | right]. case: h. - by constructor 1. - by constructor 2. - move => [sa sb sc]; constructor 3; split => //; split => // eq. move/Zo_S: xe => /setX_P [ra /setX_P [rb rc rd] re]. move/Zo_S: ye => /setX_P [ra' /setX_P [rb' rc' rd'] re']. by case: eab; apply: pair_exten => //; apply: pair_exten. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)