proposition: Lemma ltxwf t : P t.
proof: Proof. elim: n P ih t => [|k wih] Pn kih t; last have [a {}t] := tupleP t. by rewrite tuple0; apply/kih=> t2; rewrite tuple0. elim/wf: a t => a iha t; elim/wih: t => t iht. apply/kih => t'; have [a' {}t'] := tupleP t'; rewrite [_ < _]ltxi_cons. by case: (comparableP a a') => //= [/iha/(_ t')|<- /iht]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset order) mathcomp(ssralg)