proposition: Lemma orthogonal_union_order r r': order r -> order r' -> substrate r = substrate r' -> orthogonal_order r r' -> (total_order (r \cup r') /\ substrate (r \cup r') = substrate r).
proof: Proof. move => or or' ss otr; set r'' := r \cup r'. have gu: sgraph r'' by apply: setU2_graph; fprops. have sr1: substrate r'' = substrate r. set_extens t. move /(substrate_P gu). case; case => [y];case /setU2_P => h; try substr_tac;rewrite ss; substr_tac. move => tsr; apply /(substrate_P gu);left. by exists t; apply /setU2_P; left; order_tac. suff ors: order (r \cup r'). split => //; split; first by exact. rewrite sr1 => x y xsr ysr; case: (equal_or_not x y) => exy. rewrite -exy; left; order_tac; ue. move: (otr _ _ xsr ysr exy) => [h _]. rewrite/ocomparable /gle /related /r''; aw; case:h; case => cxy; try (solve [left; fprops]); right; fprops. split => //. by hnf;rewrite sr1 => y ysr; apply /setU2_P;left; order_tac. move => y x z; case /setU2_P => le1; case /setU2_P => le2; apply /setU2_P. - left; order_tac. - have xsr: inc x (substrate r) by substr_tac. have ysr: inc y (substrate r) by substr_tac. have zsr: inc z (substrate r) by rewrite ss; substr_tac. case: (equal_or_not x z) => exz; first by rewrite exz; left; order_tac. move: (otr _ _ xsr zsr exz) => [h1 _]. case: h1; case => cxz; try (by left); try (by right). case: (equal_or_not z y) => zy; first by rewrite zy; left. move: (otr _ _ zsr ysr zy) => [_]; case;split; last by right. left; move: cxz; rewrite /gle/related => cxz; order_tac. case: (equal_or_not x y) => yx; first by rewrite yx; right. move: (otr _ _ xsr ysr yx) => [_]; case; split; first by left. right; move: cxz; rewrite /gle/related => cxz; order_tac. - have xsr: inc x (substrate r) by rewrite ss; substr_tac. have ysr: inc y (substrate r) by rewrite ss; substr_tac. have zsr: inc z (substrate r) by substr_tac. case: (equal_or_not x z) => exz; first by rewrite exz; left; order_tac. move: (otr _ _ xsr zsr exz) => [h1 _]. case: h1; case => cx; try (by left); try (by right). case: (equal_or_not x y) => xy; first by rewrite xy; left. move: (otr _ _ xsr ysr xy) => [_]; case; split;last by left. right; move: cx; rewrite /gle/related => cxz; order_tac. case: (equal_or_not z y) => zx; first by rewrite zx; right. move: (otr _ _ zsr ysr zx) => [_]; case; split;first by right. left; move: cx; rewrite /gle/related => cxz; order_tac. - right; order_tac. move => x y; case /setU2_P => le1; case /setU2_P=> le2; try order_tac. ex_middle xney. have xsr: inc x (substrate r) by substr_tac. have ysr: inc y (substrate r) by substr_tac. have pa: ocomparable r x y by left. have pb: ocomparable r' x y by right. by move: (otr _ _ xsr ysr xney) => [_]; case. ex_middle xney. have xsr: inc x (substrate r) by substr_tac. have ysr: inc y (substrate r) by substr_tac. have pa: ocomparable r x y by right. have pb: ocomparable r' x y by left. by move: (otr _ _ xsr ysr xney) => [_]; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)