proposition: Lemma osum_increasing2 r f g: worder r -> substrate r = domain f -> substrate r = domain g -> (forall x, inc x (domain f) -> (Vg f x) <=o (Vg g x)) -> (osum r f) <=o (osum r g).
proof: Proof. move=> wor sf sg alo. have ha: worder_on r (domain g) by []. have hb: worder_on r (domain f) by []. apply /ordinal_le_P0; apply /order_le_compatible1. apply: orsum_wor => //; aw; trivial. hnf; aw;move=> i idf; rewrite ! LgV//; fprops; move: (alo _ idf) => [aa bb _]; fprops. apply: orsum_wor => //;aw; trivial. hnf; aw;rewrite - sg sf; move=> i idf; rewrite LgV//. move: (alo _ idf) => [aa bb _]; fprops. by rewrite - sg sf. apply osum_increasing1. - split => //;aww; hnf; aw. move=> i idf; rewrite LgV//; move: (alo _ idf) =>[aa bb _]; fprops. - rewrite /Lgcomp - sg sf;split;fprops;hnf; aw; trivial. move=> i idf; rewrite LgV//; move: (alo _ idf) =>[aa bb _]; fprops. - aw => x xdf; move: (alo _ xdf) =>[aa bb le]. have xdg: inc x (domain g) by rewrite - sg sf. rewrite !LgV //; apply/order_le_compatible1; fprops. by rewrite (ordinal_o_o aa) (ordinal_o_o bb) ; apply/ordinal_le_P0. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)