proposition: Fact le0x t : [tuple of nseq n \bot] <= t :> n.-tuple T.
proof: Proof. by apply: sub_seqprod_lexi; apply: le0x (t : n.-tupleprod T). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)