proposition: Lemma OT_sum_increasing4 r f j: order r -> substrate r = domain f -> sub j (domain f) -> order_type_fam f -> (OT_sum (induced_order r j) (restr f j)) <=t (OT_sum r f).
proof: Proof. move => or sr sjf alo. have sjr: sub j (substrate r) by ue. have dr: (domain (restr f j)) = j by rewrite restr_d //. have Xa: orsum_ax r (Lg (domain f) (fun z => order_type_of (Vg f z))). split => //; hnf; aw;trivial;move=> i isf; rewrite LgV//;move: (alo _ isf) => iot. 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 pc: order_type (OT_sum r f) by apply: OT_prop1. have dj: j = domain (restr f j) by rewrite restr_d. move: (iorder_osr or sjr) => [pa' pb']. have p2: orsum_ax (induced_order r j) (Lg (domain (restr f j)) (fun z : Set => order_type_of (Vg (restr f j) z))). split;fprops;hnf;aw; trivial; move=> i idf; rewrite !LgV//. move: (sjr _ idf); rewrite sr => i1; move: (alo _ i1) => iot. by apply: OT_prop3; apply: OT_prop2. have pb: order (order_sum (induced_order r j) (Lg (domain (restr f j)) (fun z => order_type_of (Vg (restr f j) z)))). by apply: orsum_or. have pd: order_type (OT_sum (induced_order r j) (restr f j)). by apply: OT_prop1. apply /OTorder_le_altP; split => //; apply: order_le_alt4. apply /(OTorder_le_compatP pb pa). set g:= (Lg (domain f) (fun z : Set => order_type_of (Vg f z))). have fgg: fgraph g by rewrite /g; fprops. have sjdg: sub j (domain g) by rewrite /g; aw. have ->: (Lg (domain (restr f j)) (fun z => order_type_of (Vg (restr f j) z))) = restr g j. by apply: fgraph_exten;aw;fprops;rewrite /g; move => k kj /= ;rewrite !LgV//; apply: sjf. apply: osum_increasing3 => //. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)