proposition: Lemma A_bounds_V_n : forall n : nat, {s' : R1 | A s' | V n[<]s'}.
proof: Proof. intro. induction n as [| n Hrecn]. unfold V in |- *. simpl in |- *. exists s. apply s_inhabits_A. unfold dstart_l in |- *. apply shift_minus_less. apply less_plusOne. case (dif_cotrans_strong (dIntrvl n)). intro a. elim a. intros H H0. unfold V in |- *. simpl in |- *. rewrite H0. simpl in |- *. exact H. intro a. elim a. intros H H0. unfold V in |- *. simpl in |- *. rewrite H0. simpl in |- *. exact Hrecn. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon