proposition: Lemma orprod2_gleP a b: gle (order_prod2 r r') a b <-> [/\ inc a (product2 (substrate r') (substrate r)), inc b (product2 (substrate r') (substrate r))& ( (Vg a C0 = Vg b C0 /\ gle r (Vg a C1) (Vg b C1)) \/ (glt r' (Vg a C0)(Vg b C0)))].
proof: Proof. have [wor sr] := cdo_wor. have la: orprod_ax canonical_doubleton_order (variantLc r' r). by split => //; aw; fprops. apply: (iff_trans (orprod_gleP la a b)). have ->: prod_of_substrates (variantLc r' r) = (product2 (substrate r') (substrate r)). rewrite - orprod2_sr // /order_prod2 orprod_sr //. rewrite (proj2 cdo_wor). split; move => [ap2 bp2 h];split => //. case: h. move => <-; left;split => //; order_tac. by move: ap2 => / setX2_P [_ _ _]. move=> [j [ /C2_P [] ->]]; aw;first by move => h _; right. move=> p1 p2. by move: (p2 _ cdo_glt1) => p4; move: p1 => [p1 _]; left. case: h. move=> [p1 p2]; case: (equal_or_not (Vg a C1) (Vg b C1)). move:ap2 bp2 => /setX2_P [fga da Vaa VBa]. move => /setX2_P [fgb db Vab VBb]. move=> VV; left; apply: fgraph_exten =>//; first by ue. by rewrite da; move=> ix xda;try_lvariant xda. move => nVV; right; exists C1; split => //; fprops; aw; first by split. move=> i [] /cdo_gleP p3 p4; case: p3; [ | by case | by move=> [-> _]]. by move=> [r1 r2]; rewrite -r2 in r1. move => pa; right; exists C0;aw;split => //; fprops. move=> i [] /cdo_gleP []; case => // -> -> //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)