proposition: Lemma sorted_ins' s k v : sorted ord (map key s) -> sorted ord (map key (ins' k v s)).
proof: Proof. case: s=>// [[k' v']] s /= H. case: ifP=>//= H1; first by rewrite H H1. case: ifP=>//= H2; first by rewrite (eqP H2). by rewrite path_ins' //; move: (ord_total k k'); rewrite H1 H2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)