proposition: Lemma oprod_increasing4 r f j: worder_on r (domain f) -> sub j (domain f) -> ordinal_fam f -> finite_set (substrate r) -> (forall x, inc x ((domain f) -s j) -> Vg f x <> \0o) -> (oprod (induced_order r j) (restr f j)) <=o (oprod r f).
proof: Proof. move => [wor sr] sjf alo fsr alnz. have sjr: sub j (substrate r) by ue. have or: order r by move: wor => [or _]. apply /ordinal_le_P0; apply /order_le_compatible1. apply: orprod_wor. - aw; split;[ by apply: induced_wor | rewrite iorder_sr// ]. - hnf; aw; move=> i ij; rewrite LgV// ? LgV//; aw; fprops. - rewrite iorder_sr //; apply: (sub_finite_set sjr fsr). apply: orprod_wor => //; [ saw | hnf;aw ]. 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 => x xj. by rewrite /g ! LgV//; apply: sjf. apply: oprod_increasing3 => //. rewrite /g;split=> //;hnf; aw;trivial; move=> i idf; rewrite !LgV// ; fprops. by rewrite /g; aw. move => x; rewrite {1} /g; aw => xd; move: (alnz _ xd). move: xd => /setC_P [xdf _]; move: (alo _ xdf) => ov. by rewrite /g LgV // ordinal_o_sr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)