proposition: Lemma cn_sub v h x y k : valid (k.+1 \-> (x, y) \+ h) -> continuous v (k.+1 \-> (x, y) \+ h) -> oapp snd v (find k h) = x.
proof: Proof. by move=>V /(_ k (x, y)); rewrite !findPtUn2 // eqxx ltn_eqF //; apply. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)