proposition: Lemma dIntrvl_inside_l_n : forall m n : nat, m <= n -> fstT (dIntrvl m)[<=]fstT (dIntrvl n).
proof: Proof. intros. induction n as [| n Hrecn]. cut (m = 0). intro. 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 := fstT (dIntrvl n)). apply Hrecn. assumption. case (dif_cotrans_strong (dIntrvl n)). intro a. elim a. intros H3 H4. change (fstT (dIntrvl n)[<=]fstT (dif_cotrans (dIntrvl n))) in |- *. rewrite H4. simpl in |- *. astepl (fstT (dIntrvl n)[+][0]). apply plus_resp_leEq_both with (b := (sndT (dIntrvl n)[-]fstT (dIntrvl n)) [/]ThreeNZ). apply leEq_reflexive. apply less_leEq. apply div_resp_pos. apply pos_three. apply shift_zero_less_minus. apply is_interval. intro a. elim a. intros H3 H4. change (fstT (dIntrvl n)[<=]fstT (dif_cotrans (dIntrvl n))) in |- *. rewrite H4. simpl in |- *. apply leEq_reflexive. 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