proposition: Lemma tuple_to_partial_out t : [forall i in ~: s, (tuple_to_partial t) i == def].
proof: Proof. apply/forallP => i. rewrite inE. apply/implyP => si. rewrite ffunE. rewrite nth_default // leqNgt. apply: contra si => si. by rewrite -mem_enum -index_mem (leq_trans si) // size_tuple -cardE. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner