proposition: Lemma tearing_sequences_projsig (u : nat -> R) (v : R -> nat) (en : enumeration R u v) (n : nat) : let (I,pr) := tearing_sequences u v en n in proj1_sig (tearing_sequences u v en (S n)) = first_two_in_interval u v (fst I) (snd I) en pr.
proof: Proof. simpl. destruct (tearing_sequences u v en n) as [[a b] pr]. simpl. reflexivity. Qed.
imports: Coq.Reals.Rdefinitions Coq.Reals.Raxioms Rfunctions Coq.Reals.RIneq Coq.Logic.FinFun Coq.Logic.ConstructiveEpsilon