proposition: Lemma Intrvl_inside_r_n : forall (x : R1) (m n : nat), m <= n -> sndT (Intrvl x n)[<=]sndT (Intrvl x m).
proof: Proof. intros. induction n as [| n Hrecn]. cut (m = 0). intro. rewrite H0. 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. apply leEq_transitive with (sndT (Intrvl x n)). case (if_cotrans_strong x (Intrvl x n)). intro H2. elim H2. intros H3 H4. change (sndT (if_cotrans x (Intrvl x n))[<=]sndT (Intrvl x n)) in |- *. rewrite H4. apply leEq_reflexive. intro H2. elim H2. intros H3 H4. change (sndT (if_cotrans x (Intrvl x n))[<=]sndT (Intrvl x n)) in |- *. rewrite H4. astepr (sndT (Intrvl x n)[+][0]). astepl (sndT (Intrvl x n)[+] [--]((sndT (Intrvl x n)[-]fstT (Intrvl x n)) [/]ThreeNZ)). apply plus_resp_leEq_both. apply leEq_reflexive. apply inv_cancel_leEq. astepl ([0]:Q_as_COrdField). astepr ((sndT (Intrvl x n)[-]fstT (Intrvl x 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.Q_in_CReals