proposition: Lemma suppP x (s : fmap) : supp_spec x s (x \in supp s).
proof: Proof. move E: (x \in supp s)=>b; case: b E; move/idP; last first. - move=>H; apply: supp_spec_none. case E: (fnd _ _)=>[v|] //; case: H. rewrite /supp /fnd in E *; case: s E=>/=. elim=>[|[y w] s IH] H1 //=. case: ifP=>H; first by rewrite (eqP H) inE eq_refl. rewrite -topredE /= eq_sym H; apply: IH. by apply: path_sorted H1. case: s; elim=>[|[y w] s IH] /= H1 //; rewrite /supp /= inE in IH *. case: eqP=>[-> _|H] //=. - by apply: (@supp_spec_some _ _ w); rewrite /fnd /= eq_refl. move: (path_sorted H1)=>H1'; move/(IH H1'); case=>[v H2|H2]; [apply: (@supp_spec_some _ _ v) | apply: supp_spec_none]; by rewrite /fnd /=; case: eqP H=>// ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)