proposition: Lemma oprod_unit1 r g I: orprod_ax r g -> sub I (domain g) -> (forall i, inc i ((domain g) -s I) -> singletonp (substrate (Vg g i))) -> (order_prod r g) \Is (order_prod (induced_order r I) (restr g I)).
proof: Proof. move => oa sI alse; move: (oa) => [wor sr alo]. have dr: (domain (restr g I)) = I by aw. have sI1: sub I (substrate r) by ue. have [or _] := (wor). have oa': orprod_ax (induced_order r I) (restr g I). hnf; aw; rewrite iorder_sr //;split => //; first by apply: induced_wor. hnf;rewrite dr;move=> i id. rewrite LgV//; apply: (alo _ (sI _ id)). have o1: order (order_prod r g) by fprops. have o2: order (order_prod (induced_order r I) (restr g I)) by fprops. set E := substrate (order_prod r g). set F := substrate (order_prod (induced_order r I) (restr g I)). have Ep: E = prod_of_substrates g by rewrite /E orprod_sr. have Fp: F = prod_of_substrates (restr g I) by rewrite /F orprod_sr. have fg1: fgraph (fam_of_substrates (restr g I)) by rewrite /fam_of_substrates ;fprops. have fg2: fgraph (fam_of_substrates g) by rewrite /fam_of_substrates; fprops. have rd:= (restr_d g I). have ta: lf_axiom (fun z => restr z I) E F. move=> z; rewrite Ep Fp; move /prod_of_substratesP => [fgz dz iVV]. have sj2: sub I (domain z) by ue. apply /prod_of_substratesP;split;aww. by move=> i ij; rewrite ! LgV//; apply: iVV; apply: sI. have specs: forall i x y, inc i (domain g) -> ~ inc i I -> inc x E -> inc y E -> Vg x i = Vg y i. move => i x y idg nij ; rewrite Ep. move /prod_of_substratesP => [fgu du up]. move /prod_of_substratesP => [fgv dv vp]. have xc: (inc i ((domain g) -s I)) by apply /setC_P; split => //. move: (up _ idg) (vp _ idg) => pa pb. by move: (alse _ xc) => /singletonP [_]; apply. have ri: forall u v, inc u E -> inc v E -> restr u I = restr v I -> u = v. move=> u v uE vE. move: (uE)(vE); rewrite Ep. move /prod_of_substratesP => [fgu du up]. move /prod_of_substratesP => [fgv dv vp] sar. apply: fgraph_exten => //; [ ue | move => x ; rewrite du => xdg]. case: (inc_or_not x I) => xI; last by apply: specs. move: (f_equal (Vg ^~ x) sar); rewrite !LgV//. exists (Lf (fun z => restr z I) E F). hnf; saw. saw;apply: lf_bijective => //. move=> y; rewrite Ep Fp; move /prod_of_substratesP=> [fgy dy iVV]. set x := (Lg (domain g) (fun z => Yo (inc z I) (Vg y z) (rep (substrate (Vg g z))))). have fgx: fgraph x by rewrite /x; fprops. have dx: domain x = domain g by rewrite /x; aw. exists x. apply /prod_of_substratesP;split => // i idx; rewrite /x LgV //; Ytac xj. rewrite rd in iVV; move: (iVV _ xj); rewrite LgV//. have xc: (inc i ((domain g) -s I)) by apply /setC_P; split => //. by move: (alse _ xc) => /singletonP [ne1 _]; apply: rep_i. apply: fgraph_exten; fprops; rewrite dy; aw; trivial. by move => i ij; rewrite /x !LgV//; fprops; Ytac0. have sjr: sub I (substrate r) by ue. hnf; aw; move=> x y xE yE; rewrite !LfV//. move: (xE)(yE); rewrite Ep. move /prod_of_substratesP => [fgx dx xp]. move /prod_of_substratesP => [fgy dy yp]. have pa : substrate (induced_order r I) = I by rewrite iorder_sr. have sjx: sub I (domain x) by rewrite dx. have sjy: sub I (domain y) by rewrite dy. split. move /(orprod_gleP oa) => [_ _ h]; apply /(orprod_gleP oa'). rewrite -Fp;split; [by apply: ta | by apply: ta | ]. case: h; first by move=> -> ; left. move => [k [ksr klt kle]]; right; rewrite pa;exists k. case: (inc_or_not k I) => kj. hnf; rewrite !LgV//; split => // i ilt. move: (iorder_gle4 ilt) => [ij _]; rewrite !LgV//. apply: (kle _ (iorder_gle2 ilt)). by move: klt => [_ []]; apply: specs => //; rewrite - sr. move /(orprod_gleP oa') => [_ _ h]; apply /(orprod_gleP oa). rewrite -Ep; split => //; case: h; first by move => h;left; apply: ri. rewrite pa;move=> [k [ksr klt kle]]; right; exists k. rewrite sr; split; [by apply: sI | by move: klt; rewrite !LgV | ]. move=> i [lik nik]; case: (inc_or_not i I) => ij. have lik1: glt (induced_order r I) i k by split => //; apply/iorder_gleP. move: (kle _ lik1); rewrite !LgV//. apply: specs => //; rewrite - sr;order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)