proposition: Lemma cn_fresh v h x : valid h -> continuous v (fresh h \-> x \+ h) <-> continuous v h /\ last_atval v h = x.1.
proof: Proof. rewrite -(valid_fresh x (leqnn _))=>V; split; last first. - case=>C H k y; rewrite !findPtUn2 // eqSS; case: ltngtP=>N. - by rewrite ltn_eqF; [apply: C | apply: (ltn_trans N _)]. - by move/find_some /dom_ordfresh /(ltn_trans N); rewrite ltnn. by case=><-; rewrite N ltn_eqF. move=>C; split; last first. - move: (C (last_key h) x). by rewrite !findPtUn2 // eqxx ltn_eqF //; apply. move=>k w; case: (ltnP k (last_key h))=>N; last first. - by move/find_some /dom_ordfresh /(leq_ltn_trans N); rewrite ltnn. by move: (C k w); rewrite !findPtUn2 // eqSS !ltn_eqF // (ltn_trans N _). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)