proposition: Lemma oprod_increasing1 r f g: orprod_ax r f -> orprod_ax r g -> (forall x, inc x (domain f) -> (Vg f x) <=O (Vg g x)) -> (order_prod r f) <=O (order_prod r g).
proof: Proof. move => oa oa1 ale. have o1: order (order_prod r f) by fprops. have o2: order (order_prod r g) by fprops. split => //; apply: (proj33 (order_le_alt o1 o2 _)). set si:= fun j => choose (fun x => order_morphism x (Vg f j) (Vg g j)). have sip: forall j, inc j (domain f) -> order_morphism (si j) (Vg f j) (Vg g j). move=> j jdf; move:(ale _ jdf) => [p1 p2 [f0 [x [fx1 fx2]]]]. move: (isomorphism_to_morphism p1 p2 fx1 fx2) => [res _]. rewrite /si; apply choose_pr. by exists (Lf (fun z => Vf f0 z) (substrate (Vg f j)) (substrate (Vg g j))). have dfdg: domain f = domain g by move: oa oa1 => [_ s1 _] [_ s2 _]; ue. set E:= substrate (order_prod r f). set F := substrate(order_prod r g). have Ep: E = (prod_of_substrates f) by apply: orprod_sr => //. have Fp: F = (prod_of_substrates g) by apply: orprod_sr => //. set h:= fun z => Lg (domain f) (fun i => Vf (si i) (Vg z i)). have ta: lf_axiom h E F. rewrite Ep Fp ; move => t /prod_of_substratesP [fgt dt als]. apply /prod_of_substratesP. rewrite - dfdg /h; aw;split;fprops;move=> i idf; rewrite LgV//. move: (sip _ idf) => [_ _ [fsi ssi tsi] _]. by Wtac; rewrite ssi;apply: als. have hi: forall u v, inc u E -> inc v E -> h u = h v -> u = v. rewrite Ep; move=> u v / prod_of_substratesP [fgu du alu] /prod_of_substratesP [fgv dv alv] sh. apply: fgraph_exten =>//; first by ue. rewrite du; move=> x xdf; move: (f_equal (Vg ^~x) sh); rewrite /h !LgV// => sW. move: (order_morphism_fi (sip _ xdf)) => [_ insi]. move: (sip _ xdf) => [_ _ [fsi ssi tsi] _]. apply: insi =>//; rewrite ssi; [ apply: alu => // |apply: alv => //]. exists (Lf h E F); red; aw; split => //. saw;by apply: lf_function. red; aw; move=> x y xE yE; rewrite /h !LfV//. have srdf: substrate r = domain f by move: oa => [_ sr _]. move: (xE); rewrite Ep; move /prod_of_substratesP => [fgx dx alx]. move: (yE); rewrite Ep; move /prod_of_substratesP => [fgy dy aly]. split. move /(orprod_gleP oa) => [_ _ aux]; apply /(orprod_gleP oa1). rewrite -Fp;split; [by apply: ta | by apply: ta |]. case: aux; first by move=>->; left. move=> [j [jsr jlt jle]]; right; ex_tac. rewrite srdf in jsr;move: jlt; rewrite ! LgV//. move: (order_morphism_fi (sip _ jsr)) => [_ insi]. move: (sip _ jsr) => [_ _ [fsi ssi tsi] jsrp]. have vsx: inc (Vg x j) (source (si j)) by rewrite ssi; apply: alx => //. have vsy: inc (Vg y j) (source (si j)) by rewrite ssi; apply: aly => //. rewrite /glt -jsrp //;move=> [p1 p2]; split =>//; dneg sV; apply: insi =>//. move=> i ij. have idf: inc i (domain f) by rewrite - srdf; order_tac. by move: (jle _ ij); rewrite !LgV//; move=> ->. move /(orprod_gleP oa1) => [h1 h2 aux]; apply /(orprod_gleP oa). rewrite -Ep; split=> //; case: aux. move => sh; left; apply: hi =>//. move=> [j [jsr jlt jle]]; right; ex_tac. rewrite srdf in jsr; move: jlt; rewrite !LgV//. move: (sip _ jsr) => [_ _ [fsi ssi tsi] jsrp]. rewrite /glt jsrp; first by move=> [p1 p2]; split =>//; dneg sV; ue. rewrite ssi; apply: alx => //. rewrite ssi; apply: aly => //. move=> i ij. have idf: inc i (domain f) by rewrite - srdf; order_tac. move: (jle _ ij); rewrite ! LgV//. move: (order_morphism_fi (sip _ idf)) =>[_ insi]. move: (sip _ idf) => [_ _ [fsi ssi tsi] jsrp]. apply: insi; rewrite ssi;[ apply: alx => // | apply: aly => //]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)