proposition: Lemma tuple_pad_injective k n (H: n <= k): injective (tuple_pad (n:=n) ^~ H).
proof: Proof. move => l1 l2 /= sv; apply:val_inj; move /eqP: (f_equal (fun l => tval l) sv). by rewrite !tuple_pad_val eqseq_cat ?size_tuple // eqxx andbT => /eqP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)