proposition: Lemma Exercise1_4a1 r x y: order r -> inc x (substrate r) -> inc y (substrate r) -> ocomparable r x y \/ class (ncr_equiv r) x = class (ncr_equiv r) y.
proof: Proof. move => or xsr ysr. case: (p_or_not_p (ocomparable r x y)) =>h; [by left | right]. move:(ncr_properties or) => [p1 p2 p3 p4]. have: related (ncr_equiv r) x y by apply: p4; split => //; right. by move /(related_equiv_P p1) => [_ _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)