proposition: Lemma equivalence_preorder1 r: preorder r -> equivalence (equivalence_associated_o r).
proof: Proof. move=> [gr _ tr]. have gi: sgraph (opp_order r) by fprops. have gi2:= (setI2_graph2 gr (x:=r)). have gi3: sgraph (r \cap (opp_order r)). by move=> x xi; apply: gr (setI2_1 xi). apply: symmetric_transitive_equivalence => //. by move=> x y /eao_P [pa pb]; apply/eao_P. move=> x y z /eao_P [xy yx] /eao_P [yz zy]; apply/eao_P. split; [ apply: tr xy yz | apply: tr zy yx ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)