proposition: Lemma Intrvl_inside_l_n : forall (x : R1) (m n : nat), m <= n -> fstT (Intrvl x m)[<=]fstT (Intrvl x n).
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. case H0. intro H1. rewrite H1. apply leEq_reflexive. intro. apply leEq_transitive with (fstT (Intrvl x n)). apply Hrecn. assumption. case (if_cotrans_strong x (Intrvl x n)). intro H2. elim H2. intros H3 H4. change (fstT (Intrvl x n)[<=]fstT (if_cotrans x (Intrvl x n))) in |- *. rewrite H4. astepl (fstT (Intrvl x n)[+][0]). simpl. apply (plus_resp_leEq_both Q_as_COrdField). apply leEq_reflexive. apply less_leEq. apply (div_resp_pos Q_as_COrdField). apply (pos_three Q_as_COrdField). apply (shift_zero_less_minus Q_as_COrdField). apply (is_interval Q_as_COrdField). intro H2. elim H2. intros H3 H4. change (fstT (Intrvl x n)[<=]fstT (if_cotrans x (Intrvl x n))) in |- *. rewrite H4. 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.Q_in_CReals