proposition: Lemma oprod_unit2 r g I: worder_on r (domain g) -> ordinal_fam g -> sub I (domain g) -> finite_set (substrate r) -> (forall i, inc i ((domain g) -s I) -> Vg g i = \1o) -> oprod r g = oprod (induced_order r I) (restr g I).
proof: Proof. move=> [wor sr] ofg jd fs alz. have or: order r by fprops. have jsr: sub I (substrate r) by ue. have aa: substrate (induced_order r I) = I by rewrite iorder_sr. apply: ordinal_o_isu1. apply: orprod_wor => //;hnf; aw => // i idg; rewrite !LgV//; fprops. apply: orprod_wor. + by aw; split => //; apply: induced_wor. + hnf; aw => i idg; rewrite !LgV //; aww. + rewrite aa; apply: (sub_finite_set jsr fs). set g1:= Lgcomp _ _. have ->: (Lgcomp (restr g I) ordinal_o) = (restr g1 I). rewrite /g1/Lgcomp;aw; apply: Lg_exten => x xd. by rewrite !LgV // ;apply: jd. have dg1: domain g1 = domain g by rewrite /g1; aw. apply: oprod_unit1; rewrite /orprod_ax ? dg1 //. split => //;move=> i idg; rewrite /g1 !LgV//; fprops; ue. move=> i ic; move /setC_P: (ic) => [ic1 _]. by rewrite /g1 LgV// (alz _ ic) (ordinal_o_sr ); exists emptyset. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)