proposition: Lemma orthogonal_union_inter r r' (r1 := r \cup r') (r2 := r \cup opp_order r'): order r -> order r' -> substrate r = substrate r' -> orthogonal_order r r' -> [/\ total_order r1, total_order r2, substrate r1 = substrate r, substrate r2 = substrate r & r = r1 \cap r2].
proof: Proof. move => or or' ssr ort1. move: (opp_osr or') => [or'' sr'']. rewrite - ssr in sr''. have cc: forall x y, ocomparable r' x y <-> ocomparable (opp_order r') x y. move => x y; split. by case => pa; [right | left]; apply /opp_gleP. by case => pa; [right | left]; apply /opp_gleP. have ort2: orthogonal_order r (opp_order r'). move => x y xsr ysr xny; move: (ort1 _ _ xsr ysr xny). move => [pa pb]; split. by case: pa => h1; [by left | right]; apply /cc. by move => [pc pd];case:pb; split => //; apply /cc. symmetry in sr''. move: (orthogonal_union_order or or' ssr ort1); rewrite -/r1; move => [pa pb]. move: (orthogonal_union_order or or'' sr'' ort2); rewrite -/r1; move => [pc pd]. split => //. rewrite - (set_UI2r r r' (opp_order r')); symmetry; apply /setU2id_Pr. move => t /setI2_P [ta tb]. have gr': sgraph r' by fprops. move: (gr' _ ta); rewrite /pairp => pt. have le1: gle r' (P t) (Q t) by rewrite /gle/related pt. have le2: gle r' (Q t) (P t) by apply /opp_gleP; rewrite /gle/related pt. have eq1: P t = Q t by order_tac. have psr: inc (P t) (substrate r) by rewrite ssr; order_tac. by rewrite - pt -eq1; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)