proposition: Lemma cotrans_analyze_strong : forall (q1 q2 : Q_as_COrdField) (x : R1) (H : q1[<]q2), ((inj_Q R1 q1[<]x) and (cotrans_analyze x q1 q2 H[=]q1)) or (x[<]inj_Q R1 q2) and (cotrans_analyze x q1 q2 H[=]q2).
proof: Proof. intros. unfold cotrans_analyze in |- *. elim (less_cotransitive_unfolded R1 (inj_Q R1 q1) (inj_Q R1 q2) (inj_Q_less R1 q1 q2 H) x). intros. left. split. assumption. algebra. intros. right. split. assumption. algebra. Qed.
imports: CoRN.reals.Q_in_CReals