proposition: Remark trans_ltn : ssrbool.transitive ltn.
proof: Proof. by move => x y z; apply (@ltn_trans x y z). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor