proposition: Lemma isum_q7 I (s:= disjointU (restr f I)) :sub I E -> forall x y, gle (ipartial_order I) x y <-> [/\ inc x s, inc y s & glt r (Q x) (Q y) \/ Q x = Q y /\ (P x) <=o (P y)].
proof: Proof. move => seN; move: (isum_q4 seN) => ax x y. apply: (iff_trans (orsum_gleP _ _ x y)). rewrite - (orsum_sr ax) (isum_q5 seN) -/s. split; move =>[xs ys etc]; split => //; case: etc. - by move/iorder_gltP => /proj33;left. - move /isum_q6: xs =>[ra rb rc]. move => [sa]; rewrite LgV//;move/graph_on_P1 =>[ _ rd re]; right; split => //. rewrite - (proj32 fprop) in seN. move:(Os_ordinal (proj33 fprop _ (seN _ ra))) => os. by split => //; apply: os. - move => h; left; apply/iorder_gltP. by move /isum_q6: xs =>[ra _ _ ]; move /isum_q6: ys =>[rb _ _]. - move =>[ha /proj33 hb]; right; split => //. move /isum_q6: xs =>[ra rb _]. move /isum_q6: ys =>[_ ]; rewrite - ha => rc _. by rewrite LgV//; apply/graph_on_P1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)