proposition: Lemma OT_prod_increasing4 r f j: worder r -> substrate r = domain f -> sub j (domain f) -> order_type_fam f -> (forall x, inc x ((domain f) -s j) -> substrate (Vg f x) <> emptyset) -> (OT_prod (induced_order r j) (restr f j)) <=t (OT_prod r f).
proof: Proof. move => or sr sjf alo alne . have sjr: sub j (substrate r) by ue. have dr: (domain (restr f j)) = j by rewrite restr_d //. have Xa: orprod_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_prod r (Lg (domain f) (fun z => order_type_of (Vg f z)))). by apply: orprod_or. have pc: order_type (OT_prod r f) by apply: OT_prop1. have dj: j = domain (restr f j) by rewrite restr_d. have odr: order r by move: or => [ok _]. have p2: orprod_ax (induced_order r j) (Lg (domain (restr f j)) (fun z : Set => order_type_of (Vg (restr f j) z))). have woi: worder (induced_order r j) by apply:induced_wor. split => //; aw;first by rewrite iorder_sr. hnf;aw => 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_prod (induced_order r j) (Lg (domain (restr f j)) (fun z => order_type_of (Vg (restr f j) z)))). by apply: orprod_or. have pd: order_type (OT_prod (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; ue. have ->: (Lg (domain (restr f j)) (fun z=> order_type_of (Vg (restr f j) z))) = restr g j. by apply: fgraph_exten; aww;rewrite /g; move => k kj /= ;rewrite !LgV//;apply: sjf. apply: oprod_increasing3 => //. move=> x; rewrite /g Lgd => xg. have xdf: inc x (domain f) by move: xg => /setC_P []. aw; rewrite LgV//;move: (alne _ xg) => t; dneg bad. move: (order_type_exists (OT_prop2 (alo _ xdf))) => [h [_ _ [[[fh _] _] sh tgh] _]]. apply /set0_P => t' ts. empty_tac1 (Vf h t'); rewrite - tgh; Wtac. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)