proposition: Lemma x_in_Intrvl_l : forall (x : R1) (n : nat), inj_Q R1 (fstT (Intrvl x n))[<]x.
proof: Proof. intros. induction n as [| n Hrecn]. simpl in |- *. cut ((inj_Q R1 (start_l x)[<]x) and (x[<]inj_Q R1 (start_r x))). intro H. elim H. intros. assumption. apply start_of_sequence_property. case (if_cotrans_strong x (Intrvl x n)). intro H. elim H. intros H0 H1. change (inj_Q R1 (fstT (if_cotrans x (Intrvl x n)))[<]x) in |- *. rewrite H1. simpl in |- *. assumption. intro H. elim H. intros H0 H1. change (inj_Q R1 (fstT (if_cotrans x (Intrvl x n)))[<]x) in |- *. rewrite H1. simpl in |- *. assumption. Qed.
imports: CoRN.reals.Q_in_CReals