proposition: Lemma tearing_sequences_inc_dec (u : nat -> R) (v : R -> nat) (pen : enumeration R u v) : forall n : nat, let I := proj1_sig (tearing_sequences u v pen n) in let SI := proj1_sig (tearing_sequences u v pen (S n)) in Rlt (fst I) (fst SI) /\ Rlt (snd SI) (snd I).
proof: Proof. intro n. simpl. destruct (tearing_sequences u v pen n) as [[a b] pr]. simpl. pose proof (first_two_in_interval_works u v a b pen pr). destruct (first_two_in_interval u v a b pen pr). simpl. split. - destruct H. assumption. - destruct H as [H1 [H2 [H3 [H4 H5]]]]. assumption. Qed.
imports: Coq.Reals.Rdefinitions Coq.Reals.Raxioms Rfunctions Coq.Reals.RIneq Coq.Logic.FinFun Coq.Logic.ConstructiveEpsilon