proposition: Lemma ncr_properties r: order r -> [/\ equivalence (ncr_equiv r), (substrate (ncr_equiv r) = substrate r), (forall x, inc x (substrate r) -> class (ncr_equiv r) x = ncr_component r x) & (forall x y, not_comp_rel r x y -> related (ncr_equiv r) x y)].
proof: Proof. rewrite /ncr_equiv/ncr_component=> or. have ncre: forall x y, not_comp_rel r x y -> inc x (substrate r). by move=> x y [res _]. have ncr: (reflexive_re (not_comp_rel r) (substrate r)). move => x; split; [ by move => xsr; split => //; left | by apply: ncre]. have ncs:(symmetric_r (not_comp_rel r)). move=> x y [xsr ysr]; case => aux; split => //; [ by left | right]. by move => [] h; case: aux; [right | left]. move:(chain_equivalence_eq ncr ncs ncre) => [pa pb]. split => //. + by apply: connected_comp_class. + by move => x y rxy; apply: setF_pr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)