proposition: Lemma start_of_sequence_property : forall x : R1, (inj_Q R1 (start_l x)[<]x) and (x[<]inj_Q R1 (start_r x)).
proof: Proof. intro. unfold start_l, start_r in |- *. elim start_of_sequence2; auto. Qed.
imports: CoRN.reals.Q_in_CReals