proposition: Lemma path_ins' s k1 k2 v : ord k1 k2 -> path ord k1 (map key s) -> path ord k1 (map key (ins' k2 v s)).
proof: Proof. elim: s k1 k2 v=>[|[k' v'] s IH] k1 k2 v H1 /=; first by rewrite H1. case/andP=>H2 H3; case: ifP=>/= H4; first by rewrite H1 H3 H4. case: ifP=>H5 /=; first by rewrite H1 (eqP H5) H3. by rewrite H2 IH //; move: (ord_total k2 k'); rewrite H4 H5. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)