From mathcomp.ssreflect
Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
From mathcomp
Require Import path.
From fcsl
Require Import pred prelude ordtype finmap pcm unionmap.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section Keys.
Variables (K : ordType) (V : Type) (U : union_map_class K V).
Implicit Types (k : K) (v : V) (f : U).

Lemma keys_last_mono f1 f2 k :
(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
        path oleq k (dom f1) ->
(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
        path oleq k (dom f2) ->
(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
        (forall x, x \in dom f1 -> x \in dom f2) ->
        oleq (last k (dom f1)) (last k (dom f2)).
Proof.
(* Goal: forall (_ : is_true (@path (Ordered.sort K) (@oleq K) k (@UMC.dom K V U f1))) (_ : is_true (@path (Ordered.sort K) (@oleq K) k (@UMC.dom K V U f2))) (_ : forall (x : Equality.sort (Ordered.eqType K)) (_ : is_true (@in_mem (Equality.sort (Ordered.eqType K)) x (@mem (Equality.sort (Ordered.eqType K)) (seq_predType (Ordered.eqType K)) (@UMC.dom K V U f1)))), is_true (@in_mem (Equality.sort (Ordered.eqType K)) x (@mem (Equality.sort (Ordered.eqType K)) (seq_predType (Ordered.eqType K)) (@UMC.dom K V U f2)))), is_true (@oleq K (@last (Ordered.sort K) k (@UMC.dom K V U f1)) (@last (Ordered.sort K) k (@UMC.dom K V U f2))) *)
rewrite !umEX; case: (UMC.from f1); first by move=>_ H _; apply: path_last H.
(* Goal: forall (f : @finMap_for K V (Phant (forall _ : Ordered.sort K, V))) (i : is_true (@all (Ordered.sort K) (@UMC.p K V (@UMC.sort K V U) (@UMC.class K V U)) (@supp K V f))) (_ : is_true (@path (Ordered.sort K) (@oleq K) k (@UM.dom K V (@UMC.p K V (@UMC.sort K V U) (@UMC.class K V U)) (@UM.Def K V (@UMC.p K V (@UMC.sort K V U) (@UMC.class K V U)) f i)))) (_ : is_true (@path (Ordered.sort K) (@oleq K) k (@UM.dom K V (@UMC.p K V (@UMC.sort K V U) (@UMC.class K V U)) (@UMC.from K V U f2)))) (_ : forall (x : Equality.sort (Ordered.eqType K)) (_ : is_true (@in_mem (Equality.sort (Ordered.eqType K)) x (@mem (Equality.sort (Ordered.eqType K)) (seq_predType (Ordered.eqType K)) (@UM.dom K V (@UMC.p K V (@UMC.sort K V U) (@UMC.class K V U)) (@UM.Def K V (@UMC.p K V (@UMC.sort K V U) (@UMC.class K V U)) f i))))), is_true (@in_mem (Equality.sort (Ordered.eqType K)) x (@mem (Equality.sort (Ordered.eqType K)) (seq_predType (Ordered.eqType K)) (@UM.dom K V (@UMC.p K V (@UMC.sort K V U) (@UMC.class K V U)) (@UMC.from K V U f2))))), is_true (@oleq K (@last (Ordered.sort K) k (@UM.dom K V (@UMC.p K V (@UMC.sort K V U) (@UMC.class K V U)) (@UM.Def K V (@UMC.p K V (@UMC.sort K V U) (@UMC.class K V U)) f i))) (@last (Ordered.sort K) k (@UM.dom K V (@UMC.p K V (@UMC.sort K V U) (@UMC.class K V U)) (@UMC.from K V U f2)))) *)
move=>{f1} f1 /= _ H1; case: (UMC.from f2)=>/=.
(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
- by move=>_ /allP; case: (supp f1)=>//; rewrite /oleq eq_refl orbT.
(* Goal: forall _ : is_true (orb (@eq_op (Ordered.eqType nat_ordType) x (fresh f)) (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType nat_ordType)) (@UMC.dom nat_ordType V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f)))), is_true (leq x (fresh f)) *)
by move=>{f2} f2 /= _; apply: seq_last_mono H1.
Qed.

End Keys.

(* Last_key and Fresh are constructs that work *)
(* for any union map with integer keys *)
(* Should be developed more generally for any union map class *)
(* with a proof that key U = nat, but I can't bother right now *)

Section FreshLastKey.
Variable V : Type.
Implicit Type f : union_map [ordType of nat] V.

Definition last_key f := last 0 (dom f).

Lemma last_key0 : last_key Unit = 0.
Proof. by rewrite /last_key /Unit /= !umEX. Qed.

(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
Lemma last_key_dom f : valid f -> last_key f \notin dom f -> f = Unit.
Proof.
(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
rewrite /valid /= /last_key /Unit /= !umEX /= -{4}[f]UMC.tfE.
(* Goal: forall (_ : is_true (@UM.valid (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (@pred_of_simpl nat (@predT nat)) (@UMC.from (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f))) (_ : is_true (negb (@in_mem nat (@last nat O (@UM.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (@pred_of_simpl nat (@predT nat)) (@UMC.from (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f))) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UM.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (@pred_of_simpl nat (@predT nat)) (@UMC.from (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f)))))), @eq (UMDef.tp (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@UMC.to (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V) (@UMC.from (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V) f)) (@UMC.to (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@UM.empty (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (@pred_of_simpl nat (@UMC.cond (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V))))) *)
case: (UMC.from f)=>//=; case=>s H /= H1 _ /seq_last_in.
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
rewrite /UM.empty UMC.eqE UM.umapE /supp fmapE /= {H H1}.
(* Goal: forall _ : is_true (orb (@eq_op (Ordered.eqType nat_ordType) x (fresh f)) (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType nat_ordType)) (@UMC.dom nat_ordType V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f)))), is_true (leq x (fresh f)) *)
by elim: s.
Qed.

(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
Lemma dom_last_key f :  valid f -> ~~ empb f -> last_key f \in dom f.
(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
Proof. by move=>X; apply: contraR; move/(last_key_dom X)=>->; apply/empbP. Qed.

(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
Lemma last_key_max f x : x \in dom f -> x <= last_key f.
Proof.
(* Goal: forall (_ : is_true (@in_mem (Equality.sort (Ordered.eqType (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) x (@mem (Equality.sort (Ordered.eqType (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V) f)))) (_ : @prop_in1 (Equality.sort (Ordered.eqType (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (@mem (Equality.sort (Ordered.eqType (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V) f)) (fun y : nat => is_true (leq y x)) (inPhantom (forall y : nat, is_true (leq y x)))), @eq nat (last_key f) x *)
rewrite /last_key /= !umEX; case: (UMC.from f)=>//; case=>s H _ /=.
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
rewrite /supp /ord /= (leq_eqVlt x) orbC.
(* Goal: forall _ : is_true (orb (@eq_op (Ordered.eqType nat_ordType) x (fresh f)) (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType nat_ordType)) (@UMC.dom nat_ordType V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f)))), is_true (leq x (fresh f)) *)
by apply: sorted_last_key_max (sorted_oleq H).
Qed.

Lemma max_key_last f x :
(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
        x \in dom f -> {in dom f, forall y, y <= x} -> last_key f = x.
Proof.
(* Goal: forall (_ : is_true (@in_mem (Equality.sort (Ordered.eqType (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) x (@mem (Equality.sort (Ordered.eqType (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V) f)))) (_ : @prop_in1 (Equality.sort (Ordered.eqType (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (@mem (Equality.sort (Ordered.eqType (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V) f)) (fun y : nat => is_true (leq y x)) (inPhantom (forall y : nat, is_true (leq y x)))), @eq nat (last_key f) x *)
rewrite /last_key !umEX; case: (UMC.from f)=>//; case=>s H _ /=.
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V) f), @eq nat (last_key (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V) f (@um_pts nat_ordType V (fresh f) v))) (fresh f) *)
move=>H1 /= H2; apply: sorted_max_key_last (sorted_oleq H) H1 _.
(* Goal: forall _ : is_true (orb (@eq_op (Ordered.eqType nat_ordType) x (fresh f)) (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType nat_ordType)) (@UMC.dom nat_ordType V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f)))), is_true (leq x (fresh f)) *)
by move=>z /(H2 z); rewrite leq_eqVlt orbC.
Qed.

(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
Lemma last_keyPt (x : nat) v : last_key (x \\-> v) = x.
Proof. by rewrite /last_key /um_pts /= !umEX. Qed.

Lemma hist_path f : path oleq 0 (dom f).
Proof.
(* Goal: is_true (@path (Ordered.sort nat_ordType) (@oleq nat_ordType) O (@UMC.dom (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V) f)) *)
rewrite !umEX; case: (UMC.from f)=>// {f} f /= _; case: f; case=>//= x s H.
(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
rewrite {1}/oleq /ord /= orbC -leq_eqVlt /=.
(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
by apply: sub_path H=>z y; rewrite /oleq=>->.
Qed.

Lemma last_key_mono f1 f2 :
(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
        {subset dom f1 <= dom f2} -> last_key f1 <= last_key f2.
Proof.
rewrite leq_eqVlt orbC=>H; apply: (@keys_last_mono _ _ _ f1 f2);
try by apply: hist_path.
(* Goal: forall _ : is_true (orb (@eq_op (Ordered.eqType nat_ordType) x (fresh f)) (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType nat_ordType)) (@UMC.dom nat_ordType V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f)))), is_true (leq x (fresh f)) *)
by move=>x /=; move: (H x).
Qed.

Lemma last_keyfUn f1 f2 :
(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
        valid (f1 \+ f2) -> last_key f1 <= last_key (f1 \+ f2).
(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
Proof. by move=>X; apply: last_key_mono=>x; rewrite domUn inE X => ->. Qed.

Lemma last_keyUnf f1 f2 :
(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
        valid (f1 \+ f2) -> last_key f2 <= last_key (f1 \+ f2).
Proof. by rewrite joinC; apply: last_keyfUn. Qed.

(* freshness *)

Definition fresh f := (last_key f).+1.

(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
Lemma dom_ordfresh f x : x \in dom f -> x < fresh f.
Proof. by move/last_key_max. Qed.

Lemma dom_freshn f n : fresh f + n \notin dom f.
(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
Proof. by apply: contra (@dom_ordfresh _ _) _; rewrite -leqNgt leq_addr. Qed.

Lemma dom_fresh f : fresh f \notin dom f.
Proof. by move: (dom_freshn f 0); rewrite addn0.  Qed.

(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
Lemma valid_fresh f v : valid (f \+ fresh f \\-> v) = valid f.
Proof. by rewrite joinC validPtUn dom_fresh andbT. Qed.

Lemma valid_fresh' f v i w :
(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
  valid (f \+ i \\-> w) ->
(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
  valid (f \+ fresh (f \+ i \\-> w) \\-> v).
Proof.
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V) f (@um_pts (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V i w))), is_true (@PCM.valid (union_mapPCM (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V) f (@um_pts nat_ordType V (fresh (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V) f (@um_pts (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V i w))) v))) *)
move=> W; rewrite joinC validPtUn.
(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
move: (dom_fresh (f \+ i \\-> w)); rewrite domUn inE; rewrite W/=.
(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
by rewrite negb_or=>/andP; case=>-> _;move/validL: W=>->.
Qed.

(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
Lemma last_fresh f v : valid f -> last_key (f \+ fresh f \\-> v) = fresh f.
Proof.
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V) f), @eq nat (last_key (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) V) f (@um_pts nat_ordType V (fresh f) v))) (fresh f) *)
move=>Vf; apply: max_key_last=>[|x] /=.
(* Goal: is_true (@in_mem nat (fresh f) (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))) *)
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
- by rewrite domUn inE valid_fresh Vf domPt inE eq_refl orbT.
(* Goal: forall _ : is_true (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)))) (@UMC.dom (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) (@PCM.join (union_mapPCM (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f (@um_pts nat_ordType V (fresh f) v))))), is_true (leq x (fresh f)) *)
rewrite domUn inE /= valid_fresh Vf /= domPt inE /= orbC eq_sym.
(* Goal: forall _ : is_true (orb (@eq_op (Ordered.eqType nat_ordType) x (fresh f)) (@in_mem nat x (@mem nat (seq_predType (Ordered.eqType nat_ordType)) (@UMC.dom nat_ordType V (union_mapUMC (@Ordered.clone nat nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) V) f)))), is_true (leq x (fresh f)) *)
by rewrite leq_eqVlt; case: eqP=>//= _; apply: dom_ordfresh.
Qed.

End FreshLastKey.

