proposition: Lemma ltxi_tuplePlt n T (t1 t2 : n.-tuple T) : reflect (exists2 k : 'I_n, forall i : 'I_n, (i < k)%N -> tnth t1 i = tnth t2 i & tnth t1 k < tnth t2 k) (t1 < t2).
proof: Proof. apply: (iffP (ltxi_tupleP _ _)) => [[k kP]|[k kP ltk12]]. exists k => [i i_lt|]; last by rewrite (lt_leif (kP _ _)) ?eqxx ?leqnn. by have /eqTleif->// := kP i (ltnW i_lt); rewrite ltn_eqF. by exists k => i; case: ltngtP => //= [/kP-> _|/ord_inj-> _]; apply/leifP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)