proposition: Lemma W_n_is_upper : forall n : nat, is_upper_bound R1 A (W n).
proof: Proof. intros. induction n as [| n Hrecn]. unfold W in |- *. simpl in |- *. unfold dstart_r in |- *. red in |- *. intros x H z H0. cut (is_upper_bound R1 A b0). intros H1. red in H1. apply less_transitive_unfolded with (y := b0). apply (H1 x H z). assumption. apply less_plusOne. exact Pb0. case (dif_cotrans_strong (dIntrvl n)). intro a. elim a. intros H H0. unfold W in |- *. simpl in |- *. rewrite H0. simpl in |- *. exact Hrecn. intro a. elim a. intros. unfold W in |- *. simpl in |- *. rewrite b. simpl in |- *. exact a0. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon