proposition: Lemma oprod_set1 r g i: order_on r (domain g) -> substrate r = singleton i -> ordinalp (Vg g i) -> oprod r g = Vg g i.
proof: Proof. move=> [or sr] srs otvi. have wor :=(worder_set1 (conj or srs)). have dgi: domain g = singleton i by rewrite - sr srs. have idg: (inc i (domain g)) by rewrite dgi; fprops. have ovi:= (ordinal_o_wor otvi). rewrite /oprod /Lgcomp. set g' := Lg _ _. have la: (orprod_ax r g'). rewrite /g'; split => //; first by aw; ue. hnf; aw; move=> j; rewrite dgi=> id; rewrite LgV //; fprops. have ora := (orprod_or la). have wos: worder(order_prod r g'). rewrite/g';apply: orprod_wor=> //; first by saw. hnf; aw; rewrite dgi; move=> j /set1_P ->; rewrite LgV //; fprops. rewrite srs; apply: set1_finite. apply: (ordinal_o_isu2 wos otvi). move: (orprod_sr la). set E := substrate (order_prod r g'). set F := substrate (ordinal_o (Vg g i)). have Hf: F = Vg g i by rewrite /F; apply: ordinal_o_sr. have Hf': F = substrate (Vg g' i) by rewrite /g' LgV. move=> slo; move: (slo). rewrite /prod_of_substrates/fam_of_substrates=> slo'. have dg: domain g' = singleton i by rewrite /g' Lgd. have ig: inc i (domain g') by rewrite dg; fprops. have ta: lf_axiom (Vg ^~ i) E F. move=> t te; move: te ig; rewrite slo Hf'; apply: prod_of_substrates_p. have Hc:forall a b, inc a E-> inc b E -> Vg a i = Vg b i -> a = b. move=> a b; rewrite slo' dg => aE bE sV. by apply: (setXb_exten aE bE); aw; move=> j /set1_P ->. exists (Lf (Vg ^~i) E F). hnf;rewrite /bijection_prop lf_source lf_target; split;fprops. saw;apply: lf_bijective =>//. move=> y ys; exists (cst_graph (singleton i) y); last by rewrite LgV//;fprops. rewrite slo' dg; apply /setXb_P; fprops;split;aww. by move=> j /set1_P ->; rewrite !LgV//; fprops; rewrite - Hf'. hnf; aw; move=> a b aE bE; rewrite !LfV //. have qa: fgraph (Lg (domain g') (fun j => substrate (Vg j g'))) by fprops. have aux: (ordinal_o (Vg g i)) = Vg g' i by rewrite /g' LgV. split. move/(orprod_gleP la) => [_ _]; case. have orve:= (worder_or ovi). move=> ->; order_tac. move: bE; rewrite slo'; move /setXb_P=> [fgb db]; rewrite - db => aa. have ed: inc i (domain b) by rewrite db dg Lgd; fprops. move: (aa _ ed); rewrite !LgV //. rewrite sr dgi;move=> [j [jsr]]; move /set1_P: (jsr) => <-. by move => [jle _] _; move: jle; rewrite /g' LgV // dgi. move=> h; apply /(orprod_gleP la); rewrite - slo;split => //. case: (equal_or_not a b) => ab; [left => // | right; exists i; split]. by rewrite sr. split => //; [ by rewrite - aux | dneg nab; apply: Hc =>// ]. move=> j [lji]. have : inc j (substrate r) by order_tac. by rewrite srs; move => /set1_P => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)