proposition: Lemma dom_lfresh h n : (lfresh h) .+ (2*n) \notin dom h.
proof: Proof. suff L2: forall h x, low x -> x \in dom h -> ord x (lfresh h). - apply: (contra (L2 _ _ (lfresh_low h n))). by rewrite -leqNgt leq_addr. case=>[|[s H1]] //; rewrite /supp => /= H2 x. rewrite /dom /lfresh /get_lows /low /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. by case: ifP=>E2; apply: IH=>//; move: H1; [apply: path_sorted | apply: notin_path | apply: path_sorted]. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep