proposition: Lemma dom_fresh h n : (fresh h).+n \notin dom h.
proof: Proof. suff L2: forall (h : heap) x, x \in dom h -> ord x (fresh h). - by apply: (contra (L2 _ _)); rewrite -leqNgt leq_addr. case=>[|[s H1]] //; rewrite /supp => /= H2 x. rewrite /dom /fresh /supp /=. elim: s H1 null H2 x=>[|[y d] s IH] //= H1 x. rewrite inE negb_or; case/andP=>H3 H4 z; rewrite inE. case/orP; first by move/eqP=>->{z}; apply: (path_last_nat 0). by apply: IH; [apply: path_sorted H1 | apply: notin_path H1]. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)