proposition: Lemma right_trans (e : rel T) : symmetric e -> transitive e -> right_transitive e.
proof: Proof. by move=> s t ? * x; rewrite ![e x _]s; apply: left_trans. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice) mathcomp(seq fintype)