proposition: Lemma limit_get_id l (t : tree l.*2 kv) (Ht : (max_deg t <= n)%nat) : limit_get t = t.
proof: Proof. elim: {l} l.*2 kv t Ht => [|l IH] k t. - by rewrite (tree_frontier t). - rewrite (tree_node_children t) foldr_maxnE /=. case/andP => Hdeg1 /allP-Hdeg2. rewrite -map_take take_oversize //. congr Node. apply map_id_in => /= t' ?. apply/IH/Hdeg2/mapP; by exists t'. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist