proposition: Lemma Exercise1_4a3 r x y y': order r -> inc x (substrate r) -> related (ncr_equiv r) y y' -> gle r x y -> related (ncr_equiv r) x y \/ gle r x y'.
proof: Proof. move=> or xsr ryy' xy. move: (ncr_properties or) => [p1 p2 p3 p4]. set (C:= class (ncr_equiv r) y). set (A:=Zo C (fun z => gle r x z)). set (B:=Zo C (fun z => gle r z x)). have p5: (forall u v, inc u A -> inc v B -> gle r u v \/ gle r v u). move=> u v => /Zo_hi r1 /Zo_hi r2; right; order_tac. case: (p_or_not_p (related (ncr_equiv r) x y)); first by left. move=> nxy. have ysr: (inc y (substrate r)) by apply: (arg2_sr xy). have uc: (A \cup B = class (ncr_equiv r) y). set_extens t => ts; first by case /setU2_P: ts; move /Zo_P => []. have tsr: (inc t (substrate r)). rewrite -p2;apply: (sub_class_substrate p1 ts). case: (Exercise1_4a1 or xsr tsr). case; first by move=> c1;apply: setU2_1; apply: Zo_i. by move=> c2;apply: setU2_2; apply: Zo_i. move=> c3; case: nxy. apply /(class_P p1); rewrite c3; apply /(class_P p1). by apply: symmetricity_e =>//; apply /(class_P p1). have yC: inc y C by apply /(class_P p1);apply: reflexivity_e => //; ue. have yC': inc y' C by apply /(class_P p1). case: (Exercise1_4a2 or ysr uc p5) => h. + empty_tac1 y; apply: Zo_i => //. + move: yC'; rewrite /C -uc; case /setU2_P; first by move /Zo_hi => h'; right. by rewrite h=> /in_set0. + move: h => [z] /setI2_P [] /Zo_P [zC l1] /Zo_P [_ l2]; left. rewrite (order_antisymmetry or l1 l2). by apply: symmetricity_e => //; apply /(class_P p1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)