proposition: Fact size_tuple_padl n k (l: n.-tuple 'I_3): n <= k -> size (tuple_padl k l) = k.
proof: Proof. by move/subnKC => eq1; rewrite /tuple_padl size_cat size_nseq size_tuple /=. 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)