proposition: Lemma isum_q7_lt I (s:= disjointU (restr f I)) :sub I E -> forall x y, glt (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 => h x y; move: (isum_q7 h x y) => h1. split. move => [/h1 [sa sb sc] sd]; split => //; case: sc => h3; first by left. move: h3 => [h4 h5];right; split => //; split => // sp; case: sd. move/isum_q6: sa => /proj33 px. move/isum_q6: sb => /proj33 py. by apply: pair_exten. move =>[xs ys etc]; split. apply/h1; split => //; case: etc; first by left. move =>[h3 h4]; right; split => //; apply: (proj1 h4). by move => eq; case: etc; rewrite eq; case => // _; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)