proposition: Lemma Equivalence_relS : Equivalence_rel <-> [/\ Reflexive, Symmetric & Transitive].
proof: Proof. split; last first. - case=>r s t; split; first by apply: r. by move=>Rxy; split; apply: t=>//; apply/s. case/Equivalence_relP=>r t; split=>//; last first. - by move=>x y z Ryx Rxz; rewrite (t y x Ryx). move=>x y; split. - by move=>Rxy; rewrite -(t x y Rxy); apply: r. by move=>Ryx; rewrite -(t y x Ryx); apply: r. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)