proposition: Lemma orprod_gleP r g : orprod_ax r g -> forall x x', (gle (order_prod r g) x x' <-> [/\ inc x (prod_of_substrates g), inc x' (prod_of_substrates g) & (x= x' \/ exists j, [/\ inc j (substrate r), glt (Vg g j) (Vg x j) (Vg x' j) & forall i, glt r i j -> Vg x i = Vg x' i])]).
proof: Proof. move=> la x x'. move: (la) => [wor sr alo]; move: (proj1 wor) => or. have He: domain (fam_of_substrates g) = domain g. by rewrite /fam_of_substrates; aw. have Hf: fgraph(fam_of_substrates g) by rewrite /fam_of_substrates; fprops. split. move/(orprod_gle1P la) => [xp x'p aux]; split => //. set (s := (Zo (domain g) (fun i => Vg x i <> Vg x' i))) in aux. have ssr: sub s (substrate r) by rewrite sr; apply: Zo_S. case: (emptyset_dichot s)=> nse. left; apply: (setXb_exten xp x'p). move=> i idf; ex_middle h; empty_tac1 i. by rewrite /s; apply: Zo_i; move: idf; rewrite /fam_of_substrates; aw. have [j jle] := (proj2 wor _ ssr nse). have jp :=(aux _ jle). move: jle => []; rewrite iorder_sr //;move=> js jmin. have jsr: inc j (substrate r) by apply: ssr. right; exists j; split => //; move=> i ij; ex_middle v. have iis : (inc i s) by rewrite /s; apply: Zo_i =>//;rewrite - sr;order_tac. move: (iorder_gle1 (jmin _ iis)) => aux'; order_tac. move => [xp x'p aux]; apply /(orprod_gle1P la);split => //. set s := (Zo (domain g) (fun i => Vg x i <> Vg x' i)). have ssr: (sub s (substrate r)) by rewrite sr; apply: Zo_S. move=> j []; rewrite iorder_sr //; move => js jmin. move /Zo_P: js =>[jdg Vj]. case: aux => haux; first by rewrite haux in Vj. have [i [isr lti aeq]] := haux. have iis: inc i s by move:lti => [_ ok];apply: Zo_i =>//; ue. have ij := (iorder_gle1 (jmin _ iis)). case: (equal_or_not j i) => ji; first by ue. have ltji: glt r j i by split. by case: Vj; apply: aeq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)