proposition: Lemma omg_sep_ax : seprel_axiom omg_s.
proof: Proof. rewrite /omg_s; split=>[|x y|x y|x y z] /=; first by rewrite lastatval0. - by rewrite andbC. - move=>V /andP [H _]; rewrite lastkey0 lastatval0. by case: (x in x ==> _) H=>// /(leq_trans _) ->. move=>V /andP [X Y] /andP []. rewrite !lastkeyUn !lastatvalUn !(validLE3 V). rewrite {1 2}maxnC {1 2}/maxn gtn_max leq_max /=. case: (ltngtP (last_key x) (last_key y)) X Y=>H X Y Kx Kz; rewrite ?H ?X ?(negbTE Y) fun_if if_arg ?implybT ?Kx Kz if_same //= ?andbT. by case: (x in x ==> _) Kz=>// /(ltn_trans H) ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)