proposition: Lemma connected_comp_class x: inc x E -> class (chain_equivalence R E) x = connected_comp x.
proof: Proof. move=> xE;set_extens t; rewrite /connected_comp. move=> tc;apply: setI_i. exists E; apply: Zo_i =>//; rewrite /setF; apply: Zo_i. aw; apply /setP_Ti. by move=> y z yE /setC_P []. move=> y /Zo_P [yS xy];apply: ((setF_pr3 yS xy) _ tc). move:(chain_equivalence_eq A1 A2 A3)=> [eq sr]. have cx:inc (class (chain_equivalence R E) x) (Zo setF (fun A => inc x A)). apply: Zo_i; first by apply: setF_pr4. apply/(class_P eq); rewrite - sr in xE; equiv_tac. move=> h;apply: (setI_hi h cx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)