proposition: Lemma tuple_to_partial_in t p : p \in s -> tuple_to_partial t p \in t.
proof: Proof. rewrite /tuple_to_partial ffunE -mem_enum => Hin. apply mem_nth. by rewrite size_tuple cardE index_mem. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner