proposition: Lemma Equivalence_relP : Equivalence_rel <-> Reflexive /\ left_Transitive.
proof: Proof. split=> [eqiR | [Rxx ltrR] x y z]; last by split=>// Rxy; apply: ltrR. by split=> [x | x y Rxy z]; [case: (eqiR x x x)| case: (eqiR x y z)=> _ /(_ Rxy)]. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)