proposition: Lemma ltEtprod n T (t1 t2 : n.-tuple T) : t1 < t2 = [exists i, tnth t1 i != tnth t2 i] && [forall i, tnth t1 i <= tnth t2 i].
proof: Proof. by rewrite lt_neqAle leEtprod eqEtuple negb_forall. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)