proposition: Lemma Exercise1_4b1 r x y x' y': order r -> related (ncr_equiv r) x x' -> related (ncr_equiv r) y y' -> class (ncr_equiv r) x <> class (ncr_equiv r) y -> gle r x y -> gle r x' y'.
proof: Proof. move=> or rxx' ryy' nsc xy. move: (ncr_properties or) => [p1 p2 p3 p4]. have xsr': (inc x' (substrate r)) by rewrite -p2; substr_tac. have ysr': (inc y' (substrate r)) by rewrite -p2; substr_tac. have xsr: (inc x (substrate r)) by rewrite -p2; substr_tac. have ysr: (inc y (substrate r)) by rewrite -p2; substr_tac. case: (Exercise1_4a1 or xsr' ysr'). case => // gle1. suff: related (ncr_equiv r) x y. by move /(related_equiv_P p1)=> [_ _ h]; case: nsc. case: (Exercise1_4a3 or xsr ryy' xy)=> // rxy'. have ex'x: (related (ncr_equiv r) x' x) by apply: symmetricity_e. case: (Exercise1_4a3 or ysr' ex'x gle1) => h. apply: (transitivity_e p1 rxx'); apply (symmetricity_e p1). apply: (transitivity_e p1 ryy' h). apply: (symmetricity_e p1). have -> //: x = y' by order_tac. move => sc; case: nsc; apply /(class_eq1 p1). apply: (transitivity_e p1 rxx'). have h: related (ncr_equiv r) x' y' by apply /(related_equiv_P p1); split => //; ue. by apply: (transitivity_e p1 h); apply: (symmetricity_e p1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)