proposition: Lemma Exercise4_10c r: order r -> (Ex4_10_hyp r \2c <-> exists r', [/\ substrate r' = substrate r, order r' & orthogonal_order r r']).
proof: Proof. move => or; set E := substrate r. split; last first. move => [r' [ssr or' orth]]. move: (orthogonal_union_inter or or' (sym_eq ssr) orth). set r1 := r \cup r'; set r2 := r \cup (opp_order r'). move => [to1 to2 sr1 sr2 rin]; move: (to1) (to2) => [or1 _] [or2 _]. apply: (Exercise4_10b or NS2 card2_nz). exists (variantLc r1 r2);split => //. + by hnf; aw; move => x xtp; try_lvariant xtp. + by hnf; aw; move => x xtp; try_lvariant xtp. + aw; apply: cardinal_set2; fprops. + by aw; move => x xtp; try_lvariant xtp. + by rewrite /intersectionb; aw; trivial;rewrite setIf2f; aw. move => [g [T [f [ofg alt cdg sar oif]]]]. move /(set_of_card_twoP): cdg => [iA [iB [niAB vcdg]]]. have siA: inc iA (domain g) by rewrite vcdg; fprops. have siB: inc iB (domain g) by rewrite vcdg; fprops. set rA:= Vg g iA; set rB:= Vg g iB. have toA: total_order rA by apply: alt. have toB: total_order rB by apply: alt. move: (toA) (toB) => [orA _] [orB _]. pose prA x := Vg (Vf f x) iA; pose prB x := Vg (Vf f x) iB. pose cmp x y := x = y \/ (glt rA (prA x) (prA y) /\ (glt rB (prB y) (prB x))). pose cmp' x y := [/\ inc x E, inc y E & cmp x y]. set r' := graph_on cmp E. have samer: r' = graph_on cmp' E. by set_extens t => /Zo_P [pa pb]; move /setX_P: (pa) => [pd pe pf];apply /Zo_P;split => //; move : pb => [_ _]. have rr': forall x, inc x E -> cmp x x by move => x _; left. move: (graph_on_sr rr'); rewrite -/r' => sr'. have or': order r'. apply: order_from_rel; split => //. move => y x z pa pb. case: (equal_or_not y z); [ by move => <- | move => ynz]. case: pa; [by move => ->| move => [la lb]]. case: pb; first by move => h; contradiction. move => [lc ld]; right; split; order_tac. move => x y. case; [by move => ->| move => [la _]]. case; [by move => ->| move => [lb _]]. order_tac. by move => x y _; split; left. move:(order_product_osr ofg) => [orp srp]. move: (oif) => [_ _ [ff sf tf] mn]. have ta: forall x, inc x (source f) -> inc (Vf f x) T. move: tf;rewrite (iorder_sr orp sar) => <-; move => x xsf; Wtac; fct_tac. have spra: forall x, inc x E -> (inc (prA x) (substrate rA) /\ inc (prB x) (substrate rB)). rewrite /E - sf => x xsf; move: (sar _ (ta _ xsf)). rewrite srp; move /prod_of_substratesP. by move => [fgw dw hw]; rewrite /rA/rB /prA /prB; split; apply: hw. have sprb: forall x y, inc x E -> inc y E -> gle rA (prA x) (prA y) -> gle rB (prB x) (prB y) -> gle r x y. rewrite /E - sf => x y xsf ysf cp1 cp2; rewrite (mn _ _ xsf ysf). move: (ta _ xsf) (ta _ ysf) => xa ya; apply /iorder_gle0P => //. move: sar; rewrite srp => sa1. apply /order_product_gleP;split => //; try apply:sa1 => //. rewrite vcdg; move => t; case /set2_P => -> //. have sprd: forall x y, gle r x y -> (gle rA (prA x) (prA y) /\ gle rB (prB x) (prB y)). move => x y le1. have xsf: inc x (source f) by rewrite sf; order_tac. have ysf: inc y (source f) by rewrite sf; order_tac. move: le1; rewrite (mn _ _ xsf ysf) => le1. move: (iorder_gle1 le1) => /order_product_gleP [_ _ h]. by split; apply: h. have sprc: forall x y, gle r' x y <-> cmp' x y. by move => x y; apply: graph_on_P1. exists r'; split => //. move => x y xsr ysr xny; split. move: (spra _ xsr) (spra _ ysr) => [pa pb][pc pd]. move:(proj2 toA _ _ pa pc); move:(proj2 toB _ _ pb pd) => cp1 cp2. case: (equal_or_not (prA x) (prA y)) => neA. by left;case:cp1=>cp;[left | right ];apply:sprb => //;rewrite neA;order_tac. case: (equal_or_not (prB x) (prB y)) => neB. by left;case:cp2=>cp;[left | right ];apply:sprb => //;rewrite neB;order_tac. case: cp1; case: cp2 => l1 l2. by left; left; apply: sprb. right; right; rewrite sprc;split => //; right;split => //; split => //;fprops. right; left; rewrite sprc; split => //; right;split => //; split => //;fprops. by left; right; apply: sprb. have ynx: y <> x by apply:nesym. move => [ca cb]; case:ca => ca; move: (sprd _ _ ca) => [pa pb]; case: cb; move/sprc => [_ _];case => //; move => [pc pd]; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)