proposition: Lemma dIntrvl_inside_r_n : forall m n : nat, m <= n -> sndT (dIntrvl n)[<=]sndT (dIntrvl m).
proof: Proof. intros. induction n as [| n Hrecn]. cut (m = 0). intro H0. rewrite H0. simpl in |- *. apply leEq_reflexive. apply Nat.le_0_r. assumption. cut ({m = S n} + {m <= n}). intro H0. case H0. intro H1. rewrite H1. apply leEq_reflexive. intro H2. apply leEq_transitive with (y := sndT (dIntrvl n)). case (dif_cotrans_strong (dIntrvl n)). intro a. elim a. intros H3 H4. change (sndT (dif_cotrans (dIntrvl n))[<=]sndT (dIntrvl n)) in |- *. rewrite H4. simpl in |- *. apply leEq_reflexive. intro a. elim a. intros H3 H4. change (sndT (dif_cotrans (dIntrvl n))[<=]sndT (dIntrvl n)) in |- *. rewrite H4. simpl in |- *. astepr (sndT (dIntrvl n)[+][0]). astepl (sndT (dIntrvl n)[+][--]((sndT (dIntrvl n)[-]fstT (dIntrvl n)) [/]ThreeNZ)). apply plus_resp_leEq_both. apply leEq_reflexive. apply inv_cancel_leEq. astepl ([0]:R1). astepr ((sndT (dIntrvl n)[-]fstT (dIntrvl n)) [/]ThreeNZ). apply less_leEq. apply div_resp_pos. apply pos_three. apply shift_zero_less_minus. apply is_interval. apply Hrecn. assumption. case (le_lt_eq_dec m (S n) H). intro. right. apply Nat.lt_succ_r. assumption. intro. left. assumption. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon