proposition: Lemma equiv_ltrans: left_transitive e.
proof: Proof. by apply: left_trans; [apply: equiv_sym|apply: equiv_trans]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice) mathcomp(seq fintype)