proposition: Lemma Exercise1_7a r x: right_directed r -> inc x (substrate r) -> cr_component r x = substrate r.
proof: Proof. move /right_directedP => [or rdp]. move: (cr_properties or)=> [p1 p2 p3 p4 p5] xsr. rewrite -(p4 _ xsr);apply: extensionality. rewrite -p3;apply: sub_class_substrate => //. move=> t tsr; move: (rdp _ _ xsr tsr) => [z [xz yz]]. have r1: (related (cr_equiv r) x z) by apply: p5; left. have r2: (related (cr_equiv r) t z) by apply: p5; left. apply /(class_P p1). apply: (@transitivity_e _ z) => //; apply: symmetricity_e => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)