proposition: Lemma size_ins' (x : K) v (s : seq (K*V)) : sorted ord (map key s) -> size (ins' x v s) = if x \in map key s then size s else (size s).+1.
proof: Proof. elim: s x v=>[|[k' v'] s IH] //= k v P. case: ifP=>O /=; rewrite inE eq_sym; move/path_sorted/(IH k v): (P)=>{IH} E; case: ordP O=>//= O _. - by move/notin_path/negbTE: (ord_path O P)=>->. by rewrite E; case: ifP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)