proposition: Lemma lexi_tupleP n T (t1 t2 : n.-tuple T) : reflect (exists k : 'I_n.+1, forall i : 'I_n, (i <= k)%N -> tnth t1 i <= tnth t2 i ?= iff (i != k :> nat)) (t1 <= t2).
proof: Proof. elim: n => [|n IHn] in t1 t2 *. by rewrite tuple0 [t2]tuple0/= lexx; constructor; exists ord0 => -[]. case: (tupleP t1) (tupleP t2) => [x1 {}t1] [x2 {}t2]. rewrite [_ <= _]lexi_cons; apply: (iffP idP) => [|[k leif_xt12]]. case: comparableP => //= [ltx12 _|-> /IHn[k kP]]. exists ord0 => i; rewrite leqn0 => /eqP/(@ord_inj n.+1 i ord0)->. by apply/leifP; rewrite !tnth0. exists (lift ord0 k) => i; case: (unliftP ord0 i) => [j ->|-> _]. by rewrite !ltnS => /kP; rewrite !tnthS. by apply/leifP; rewrite !tnth0 eqxx. have /= := leif_xt12 ord0 isT; rewrite !tnth0 => leif_x12. rewrite leif_x12/=; move: leif_x12 leif_xt12 => /leifP. case: (unliftP ord0 k) => {k} [k-> /eqP<-{x2}|-> /lt_geF->//] leif_xt12. rewrite lexx implyTb; apply/IHn; exists k => i le_ik. by have := leif_xt12 (lift ord0 i) le_ik; rewrite !tnthS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)