proposition: Lemma cr_properties r: order r -> [/\ equivalence (cr_equiv r) , (forall x y, ocomparable r x y -> (inc x (substrate r)/\ inc y (substrate r))), substrate (cr_equiv r) = substrate r, (forall x, inc x (substrate r) -> class (cr_equiv r) x = cr_component r x) & (forall x y, ocomparable r x y -> related (cr_equiv r) x y)].
proof: Proof. move=> or. rewrite /cr_equiv /cr_component. have crs: (forall x y, ocomparable r x y -> (inc x (substrate r) /\ inc y (substrate r))). by move=> x y; case; split; order_tac. have rc: (reflexive_re (ocomparable r) (substrate r)). by move => x; split ; [ move=> xsr;left | case=> aux]; order_tac. have sc: (symmetric_r (ocomparable r)) by move=> x y; case; [right | left]. have crs': (forall x y, ocomparable r x y -> inc x (substrate r)). by move=> x y xy; move: (crs _ _ xy) => [ok _]. move:(chain_equivalence_eq rc sc crs') => [ha hb]. split => //. - by move=> x xsr; apply: connected_comp_class. - move => x y cr;apply /Zo_P; split. by move: (crs _ _ cr) => [xs ys]; apply: setXp_i. by aw; exists (chain_pair x y). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)