proposition: Lemma left_trans (e : rel T) : symmetric e -> transitive e -> left_transitive e.
proof: Proof. by move=> s t ? * ?; apply/idP/idP; apply: t; rewrite // s. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice) mathcomp(seq fintype)