proposition: Lemma Exercise1_4c1 r x: order r -> greatest r x -> ncr_component r x = singleton x.
proof: Proof. move => or [xsr xge]. move: (ncr_properties or) => [p1 p2 p3 p4]. rewrite -(p3 _ xsr); apply set1_pr. apply /(class_P p1); apply: reflexivity_e => //; ue. have xt: forall t, not_comp_rel r t x -> t = x. by move => u [q1 q2 h]; case: h; [ move=> -> | case;left; apply: xge ]. move => z /(class_P p1) r1; move: (symmetricity_e p1 r1). move /Zo_P => [] /setXp_P; aw; move => _ [c [cc <- tc]]. move: c cc tc. elim => u v /=; first by move => h1 h2; rewrite h2 in h1; apply: (xt _ h1). by move=> h1 [h2 h3] h4; rewrite (h1 h3 h4) in h2; apply: xt. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)