fact: Definition omg_s := fun x y : U => [&& last_atval false x ==> (last_key y < last_key x) & last_atval false y ==> (last_key x < last_key y)].
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)