proposition: Lemma dl_less_dr : dstart_l[<]dstart_r.
proof: Proof. apply less_transitive_unfolded with (y := b0). unfold is_upper_bound in bounded_above. cut (forall x : R1, A x -> forall z : R1, z[<]x -> z[<]b0). intro H. cut (forall z : R1, z[<]s -> z[<]b0). intro H0. apply H0. unfold dstart_l in |- *. apply shift_minus_less. apply less_plusOne. intros. apply H with (z := z) (x := s). apply Ps. assumption. exact Pb0. unfold dstart_r in |- *. apply less_plusOne. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon