proposition: Lemma OT_sum_increasing2 r f g: order r -> substrate r = domain f -> substrate r = domain g -> (forall x, inc x (domain f) -> (Vg f x) <=t (Vg g x)) -> (OT_sum r f) <=t (OT_sum r g).
proof: Proof. move=> wor sf sg alo. have Xa: orsum_ax r (Lg (domain f) (fun z : Set => order_type_of (Vg f z))). split => //;hnf; aw; trivial;move=> i isf; rewrite LgV//. move: (alo _ isf) => [pa pb _]. by apply: OT_prop3; apply: OT_prop2. have Xb: orsum_ax r (Lg (domain g) (fun z : Set => order_type_of (Vg g z))). split => //; hnf;aw; trivial;rewrite - sg sf. move=> i isf; rewrite LgV //; move: (alo _ isf) => [pa pb _]. by apply: OT_prop3; apply: OT_prop2. have pa:order (order_sum r (Lg (domain f) (fun z => order_type_of (Vg f z)))). by apply: orsum_or. have pb:order (order_sum r (Lg (domain g) (fun z => order_type_of (Vg g z)))). by apply: orsum_or. have pc: order_type (OT_sum r f) by apply: OT_prop1. have pd: order_type (OT_sum r g) by apply: OT_prop1. apply / OTorder_le_altP;split =>// ; apply: order_le_alt4. apply /(OTorder_le_compatP pa pb); apply:osum_increasing1 => //. aw; move=> x xdf; rewrite !LgV//; last by rewrite - sg sf. move: (alo _ xdf); move /OTorder_le_alt2P=> [ot1 ot2]. by move /(OTorder_le_compatP (OT_prop2 ot1) (OT_prop2 ot2)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)