proposition: Lemma equivalence_rel3P R : equivalence_rel R <-> [/\ reflexive R, symmetric R & transitive R].
proof: Proof. rewrite equivalence_relP; split=> [[Rrefl Rltrans]|[Rrefl Rsym Rtrans]]. by split=> //; [apply: refl_left_trans_sym | apply: left_trans_trans]. by split=> //; apply: left_trans. Qed.
imports: mathcomp(all_ssreflect) extra