proposition: Lemma osum_increasing4 r f j: worder_on r (domain f) -> sub j (domain f) -> ordinal_fam f -> (osum (induced_order r j) (restr f j)) <=o (osum r f).
proof: Proof. move => [wor sr] sjf alo. have sjr: sub j (substrate r) by ue. have or: order r by move: wor => [or _]. have dr: (domain (restr f j)) = j by aw. have ha:worder_on r (domain f) by []. rewrite /osum; apply /ordinal_le_P0; apply /order_le_compatible1. apply: orsum_wor. by aw;split;[ apply: induced_wor => // ue | rewrite iorder_sr // dr]. hnf; rewrite /Lgcomp dr; aw; move=> i ij; rewrite ! LgV //; fprops. apply: orsum_wor => //; hnf; aw; trivial;move=> i idf; rewrite !LgV//; fprops. set g:= (Lgcomp f ordinal_o). have ->: (Lgcomp (restr f j) ordinal_o) = restr g j. rewrite /Lgcomp; aw;apply: Lg_exten. by rewrite /g;red; aw;move => x xj; rewrite !LgV//; apply: sjf. apply: osum_increasing3 => //. rewrite /g;red; aw;split => //; hnf;aw; move=> i idf; rewrite LgV//; fprops. by rewrite /g; aw. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)