proposition: Lemma isum_p10 f E1 E2 r: worder r -> sub E1 E2 -> sub E2 (substrate r) -> [/\ fgraph f, domain f = substrate r & allf f ordinalp] -> ipartial_sum f r E1 <=o ipartial_sum f r E2.
proof: Proof. move => wor s12 s2r [fa fb fc]. pose g1 := Lg (substrate r) (fun i => Yo (inc i E1) (Vg f i) \0o). pose g2 := Lg (substrate r) (fun i => Yo (inc i E2) (Vg f i) \0o). have ax1: [/\ fgraph g1, domain g1 = substrate r & allf g1 ordinalp]. rewrite/g1; split; aww; hnf; aw => x xs; rewrite LgV//. Ytac h; [ apply: fc; ue | exact OS0]. have ax2: [/\ fgraph g2, domain g2 = substrate r & allf g2 ordinalp]. rewrite/g2; split; aww; hnf; aw => x xs; rewrite LgV//. Ytac h; [ apply: fc; ue | exact OS0]. have g1p i: inc i (substrate r -s E1) -> Vg g1 i = \0o. by move =>/setC_P [xe bad]; rewrite /g1 LgV //; Ytac0. have g2p i: inc i (substrate r -s E2) -> Vg g2 i = \0o. by move =>/setC_P [xe bad]; rewrite /g2 LgV//; Ytac0. have l12 x: inc x (substrate r) -> Vg g1 x <=o Vg g2 x. rewrite /g1 /g2 => xe; rewrite !LgV//; Ytac h. rewrite (Y_true (s12 _ h)); apply: oleR; apply: fc; ue. by apply: ole0x; Ytac h2; [ apply: fc; ue | apply: OS0]. have g1v: (restr g1 E1) = restr f E1. by apply: Lg_exten=> t te;rewrite /g1 LgV//;[ Ytac0 | apply: s2r; apply: s12]. have g2v: (restr g2 E2) = restr f E2. by apply: Lg_exten => t te; rewrite /g2 LgV; [ Ytac0 | apply: s2r]. move: (isum_p8 wor (proj31 ax1) (proj31 ax2) (proj32 ax1) (proj32 ax2) l12). rewrite (isum_p9 wor (sub_trans s12 s2r) ax1 g1p) (isum_p9 wor s2r ax2 g2p). by rewrite /ipartial_sum g1v g2v. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)