proposition: Lemma dom_hfresh h n : (hfresh h) .+ (2*n) \notin dom h.
proof: Proof. suff L2: forall h x, high x -> x \in dom h -> ord x (hfresh h). - apply: (contra (L2 _ _ (hfresh_high h n))). by rewrite -leqNgt leq_addr. case=>[|[s H1]] //; rewrite /supp => /= H2 x. rewrite /dom /hfresh /get_highs /high /supp -topredE /=. elim: s H1 null H2 x=>[|[y d] s IH] //= H1 x. rewrite inE negb_or; case/andP=>H3 H4 z /= E; rewrite inE. case/orP=>H5. - rewrite -!{H5 y}(eqP H5) E in H1 H3 *. by apply: (path_last 1); apply: path_filter. case: ifP=>E2; last by apply: IH=>//; apply: path_sorted H1. move: H1. have [t -> H1]: exists t, y = t .+ 1. - case: y {H3} E2; case=>[|m] //. by exists (ptr_nat m); rewrite /ptr_offset /= addn1. apply: IH=>//; first by apply: path_sorted H1. apply: notin_path; apply: ord_path H1. by case: t=>m; rewrite /ord /= addn1. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep