proposition: Lemma leqt_trans m : transitive (@leqt m).
proof: Proof. move=>t2 t1 t3 /leqtP Ht1t2 /leqtP Ht2t3. apply/leqtP => a b aLb t2aLt2b. by apply: Ht2t3 => //; apply: Ht1t2. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)