proposition: Lemma Exercise1_4a2 r y: order r -> inc y (substrate r) -> forall a b, a \cup b = class (ncr_equiv r) y -> (forall u v, inc u a -> inc v b -> ocomparable r u v) -> [\/ a = emptyset, b = emptyset | nonempty (a \cap b)].
proof: Proof. move=> or ysr a b uab h. case: (emptyset_dichot a)=> nea; first by apply: Or31. case: (emptyset_dichot b)=> neb; first by apply: Or32. move : nea neb (ncr_properties or) => [A Aa] [B Bb] [p1 p2 p3 p4]. have uc: classp (ncr_equiv r) (a \cup b). rewrite uab; apply: class_class => //; ue. have:(related (ncr_equiv r) A B). apply /(in_class_relatedP p1); exists (a \cup b); split;fprops. move /Zo_P; aw; move => [] /setXp_P [Asr Bsr] [x [xc hx tx]]. have ha: (inc (chain_head x) a) by ue. have tb: (inc (chain_tail x) b) by ue. clear hx tx; apply:Or33. have [u [v [ua vb uv]]]: exists u v, [/\ inc u a, inc v b & (not_comp_rel r) u v]. elim:x xc ha tb => u v r1 r2 r3; first by exists u,v. move: r2 r3; simpl; move=> [r0 r2] r3 r4. case: (inc_or_not (chain_head v) a); first by move=> r5; apply: r1. have uu: inc u (a \cup b) by fprops. set (w := (chain_head v)). move=> nwa; exists u, w => //. suff: inc w (a \cup b) by case/setU2_P. apply: (rel_in_class2 p1 uc). move: (rel_in_class p1 uc uu) (p4 _ _ r0) => pa pb; equiv_tac. move: (h _ _ ua vb) uv => aux [_ _]; case => // cv. exists u; apply: setI2_i => // ; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)