proposition: Lemma hfresh_high h n : high (hfresh h) .+ (2*n).
proof: Proof. rewrite /hfresh /high /get_highs. case: h n=>[n|]. - by rewrite /null /= add0n -addnA -modnDm modnDl modnMr addn0. case; rewrite /supp /high /=. elim=>[|[[x] v] h IH] /=. - by move=>_ _ n; rewrite add0n -addnA -modnDm modnDl modnMr addn0. rewrite inE negb_or ptrE /=; move/path_sorted=>H1; case/andP=>H2 H3. case: ifP=>E n /=; last by apply: IH. set f := fun x => (nat_ptr x + 2 + 2 * n) %% 2. have F: f (ptr_nat x) = f (null .+ 1). - rewrite /f -modn_mod /= add0n -addnA. rewrite -modnDm -(eqP E) modn_mod. by rewrite modnDm addnA. move: (last_inv (f := f) (x1 := (ptr_nat x)) (x2 := null .+ 1))=>L. by rewrite /f /= in L; rewrite {}L //; apply: IH. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep