proposition: Lemma isum_p8 f g r: worder r -> fgraph f -> fgraph g -> domain f = substrate r -> domain g = substrate r -> (forall x, inc x (substrate r) -> Vg f x <=o Vg g x) -> ipartial_sum f r (substrate r) <=o ipartial_sum g r (substrate r).
proof: Proof. move => wor fgf fgg df dg le1. have fp: [/\ fgraph f, domain f = substrate r & allf f ordinalp]. by split => // t; rewrite df => /le1 /proj31. have gp: [/\ fgraph g, domain g = substrate r & allf g ordinalp]. by split => // t; rewrite dg => /le1 /proj32. rewrite 2! isum_p0. pose rr := (@sub_refl (substrate r)). move: (isum_q2 wor fp rr)(isum_q2 wor gp rr) => wo1 wo2. apply: (order_cp2 wo1 wo2). apply/(order_cp0 (proj1 wo1) (proj1 wo2)) => x y. have aux : sub (disjointU (restr f (substrate r))) (disjointU (restr g (substrate r))). move => t /isum_q6 [sa sb sc]; apply/isum_q6; split => //. move:(le1 _ sa) => le2; move: (le2) => [oa ob _]. by apply/(oltP ob); apply: olt_leT le2; apply/(oltP oa). move/(isum_q7 wor fp rr) =>[xd yd cxy]. by apply/(isum_q7 wor gp rr); split => //; apply: aux. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)