proposition: Lemma oprod_increasing3 r f j: orprod_ax r f -> sub j (domain f) -> (forall x, inc x ((domain f) -s j) -> substrate (Vg f x) <> emptyset) -> (order_prod (induced_order r j) (restr f j)) <=O (order_prod r f).
proof: Proof. move=> oa jd anot. move: (oa) => [or sr alo]. set (g:= Lg (domain f) (fun z => Yo (inc z j) (Vg f z) (ordinal_o \1o))). have dfdg: domain f = domain g by rewrite /g; aw. have oa': orprod_ax r g. hnf; rewrite /order_fam /allf - dfdg;split => //. move=> i idg; rewrite /g LgV//; Ytac ij; first by apply: alo. by apply: (ordinal_o_or). have sjd': sub j (domain g) by ue. have cz: (forall i, inc i ((domain g) -s j) -> singletonp (substrate (Vg g i))). move=> i /setC_P;rewrite -dfdg /g; move=> [idf nij]; rewrite LgV//; Ytac0. by rewrite (ordinal_o_sr); exists emptyset. move: (oprod_unit1 oa' sjd' cz). have ->: (restr f j = restr g j). apply: Lg_exten; aw; move=> x xj; move: (jd _ xj) => xdf. by rewrite /g LgV//; Ytac0. move=> oi1. have oi2: (order_prod r f) \Is (order_prod r f). by apply: orderIR; apply: orprod_or. apply /(order_le_compatible oi1 oi2). apply: oprod_increasing1 => //. rewrite -dfdg; move=> x xdg; rewrite /g LgV//. Ytac nij; first by apply: order_leR=>//; apply: alo. have p2: order (Vg f x) by move: oa => [q1 q2 q4]; apply: q4. have [y yd]: nonempty (substrate (Vg f x)). case: (emptyset_dichot (substrate (Vg f x))) => // p1. have xcz: inc x ((domain f) -s j) by apply /setC_P. move: (anot _ xcz) => p4; contradiction. have s1: sub (singleton y) (substrate (Vg f x)) by apply: set1_sub. set h:= Lf (fun z => y) (singleton emptyset) (singleton y). have ta: lf_axiom (fun _ : Set => y) (singleton emptyset) (singleton y). move=> t _ /=; fprops. split => //; [fprops | exists h; exists (singleton y); split => //]. rewrite /h;split;fprops. apply (proj1 (iorder_osr p2 s1)). rewrite iorder_sr // ordinal_o_sr. saw; apply: lf_bijective => //. by move=> u v /set1_P -> /set1_P ->. move=> u /set1_P ->; exists emptyset; [fprops | done]. move => u v;rewrite lf_source => aa bb; rewrite ! LfV//. move: aa bb => /set1_P -> /set1_P ->. split; move => _. by apply /iorder_gle0P; fprops; order_tac. rewrite / \1o/ \1c;apply /ordo_leP;split;fprops. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)