proposition: Lemma cm_fresh v0 vn h x : complete v0 (fresh h \-> x \+ h) vn <-> vn = x.2 /\ complete v0 h x.1.
proof: Proof. split. - by case=>/validR V /gp_fresh G /(cn_fresh V) []; rewrite lastatval_fresh. case=>-> [V] /(gp_fresh x) G C E; split=>//; by [rewrite valid_fresh | apply/(cn_fresh V) | rewrite lastatval_fresh]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)