proposition: Lemma zip_unit_sorted' s : sorted ord (map key s) -> sorted ord (map key (zip_unit' s)).
proof: Proof. rewrite (_ : map key s = map key (zip_unit' s)) //. by apply: (map_key_zip' (s2:=s)); apply: zip_unitL'. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)