proposition: Lemma first_in_holed_interval_works (u : nat -> R) (v : R -> nat) (a b h : R) (pen : enumeration R u v) (plow : Rlt a b) : let (c,_) := first_in_holed_interval u v a b h pen plow in forall x:R, Rlt a x -> Rlt x b -> x <> h -> x <> u c -> c < v x.
proof: Proof. destruct (first_in_holed_interval u v a b h pen plow) as [c [_ beyond]]. destruct pen as [uv _]. intros x H H0 H1 x_uc. assert (ihi : in_holed_interval a b h u (v x)). { split. - rewrite -> uv. assumption. - rewrite -> uv. split; assumption. } destruct (proj1 (Nat.lt_eq_cases _ _) (beyond (v x) ihi)) as [lcvx | ecvx]. - exact lcvx. - exfalso. apply x_uc. rewrite ecvx. rewrite -> uv. reflexivity. Qed.
imports: Coq.Reals.Rdefinitions Coq.Reals.Raxioms Rfunctions Coq.Reals.RIneq Coq.Logic.FinFun Coq.Logic.ConstructiveEpsilon