proposition: Lemma lfresh_low h n : low (lfresh h) .+ (2*n).
proof: Proof. rewrite /lfresh /low /get_lows. case: h; first by rewrite modnDl modnMr. case; rewrite /supp /low /=. elim=>[|[[x] v] h IH] /=; first by rewrite modnDl modnMr. rewrite inE negb_or ptrE /=; move/path_sorted=>H1; case/andP=>H2 H3. case: ifP=>E /=; last by apply: IH. set f := fun x => (nat_ptr x + 2 + 2 * n) %% 2. have F: f (ptr_nat x) = f null. - by rewrite /f -modn_mod -addnA -modnDm -(eqP E) !modn_mod. move: (last_inv (f := f) (x1 := (ptr_nat x)) (x2 := null))=>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