proposition: Lemma osum_increasing3 r f j: orsum_ax r f -> sub j (domain f) -> (order_sum (induced_order r j) (restr f j)) <=O (order_sum r f).
proof: Proof. move=> oa jd. move: (proj1 (proj1 set0_wor)) => eo. move: (oa) => [or sr alo]. set (g:= Lg (domain f) (fun z => Yo (inc z j) (Vg f z) emptyset)). have dfdg: domain f = domain g by rewrite /g; aw. have oa': orsum_ax r g. split => //; first by ue. hnf; rewrite - dfdg /g;move=> i idg; rewrite LgV//; Ytac ij;first by apply: alo. done. have sjd': sub j (domain g) by ue. have cz: (forall i, inc i ((domain g) -s j) -> Vg g i = \0o). by move=> i /setC_P; rewrite -dfdg /g; move=> [idf nij]; rewrite LgV//; Ytac0. move: (osum_unit1 oa' sjd' cz). have ->: (restr f j = restr g j). apply: Lg_exten => s sj;rewrite LgV//; rewrite /g; [ by Ytac0 | by apply:jd ]. move=> oi1. have oi2: (order_sum r f) \Is (order_sum r f). by apply: orderIR; apply: orsum_or. apply /(order_le_compatible oi1 oi2). apply: osum_increasing1 => //. rewrite -dfdg; move=> x xdg; rewrite /g LgV//. Ytac xj; first by apply: order_leR=>//; apply: alo. split; fprops;exists (identity emptyset); exists emptyset. have auw: sub emptyset (substrate (Vg f x)) by fprops. split => //; split;fprops. - apply: (proj1 (iorder_osr _ auw)); fprops. - rewrite (iorder_sr (alo _ xdg)) // (proj2 set0_wor); apply: identity_bp. - by move=> u v; rewrite identity_s => /in_set0. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)