proposition: Lemma singleton_component A: sub A E -> ( (inc A (quotient (chain_equivalence R E) ) /\ singletonp A) <-> (exists2 a, A = singleton a & forall b, R a b -> a = b)).
proof: Proof. move=> AE. move:(chain_equivalence_eq A1 A2 A3)=> [eq sr]. split. move=> [Asq [x Asx]]; exists x => //. move=> b /setF_pr0. move /(in_class_relatedP eq) => [y [cy xy]]. have <- : A = y. move: Asq => /(setQ_P eq) => cA; case: (class_dichot eq cy cA)=> //. move=> dy; red in dy; empty_tac1 x; apply:setI2_i => //. rewrite Asx; fprops. by rewrite Asx; move /set1_P. move=> [x As Ap]; rewrite As; split; last by exists x. have xse: inc x (substrate (chain_equivalence R E)). rewrite sr; apply: AE; rewrite As; fprops. have Aq: forall b, R b x -> b = x. by move => b ba; rewrite (Ap b) //; apply: A2. suff: (class (chain_equivalence R E) x = singleton x). move => <-; apply /(setQ_P eq); apply: (class_class eq xse). apply: set1_pr; first by apply /(class_P eq); equiv_tac. move => w; move /(class_P eq) => /(proj44 eq). move/graph_on_P1 => [ pa qa [c [cc <-]]]. elim: c cc. by move=> u v /= uv vx; rewrite vx in uv; apply: Aq. by move=> p c h1 /= [Rp cc] tc; apply: Aq; rewrite - (h1 cc tc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)