fact: Definition leqt m (t1 t2 : m.-tuple A) := [forall a : 'I_m, forall b : 'I_m, (a <= b) ==> (tnth t1 a <= tnth t1 b)%O ==> (tnth t2 a <= tnth t2 b)%O].
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)