proposition: Theorem start_of_sequence : forall x : R1, {q1 : Q_as_COrdField | {q2 : Q_as_COrdField | inj_Q q1 [<] x | x [<] inj_Q q2}}.
proof: Proof. intros. cut {n : nat | x [<] nring (R:=R1) n}. intro H. cut {n : nat | [--]x [<] nring (R:=R1) n}. intro H0. case H. intro n2. intro. case H0. intro n1. intro. exists (Qmake (- n1) 1). exists (Qmake n2 1). simpl in |- *. rstepl (zring (R:=R1) (- Z_of_nat n1)). astepl [--](nring (R:=R1) n1). apply inv_cancel_less. astepr (nring (R:=R1) n1). assumption. simpl in |- *. rstepr (zring (R:=R1) (Z_of_nat n2)). astepr (nring (R:=R1) n2). assumption. apply Archimedes'. apply Archimedes'. Qed.
imports: CoRN.model.reals.Cauchy_IR CoRN.model.monoids.Nmonoid CoRN.model.rings.Zring CoRN.algebra.CRing_Homomorphisms CoRN.algebra.Expon Coq.QArith.Qpower CoRN.tactics.CornTac