proposition: Lemma trichotomy_strong1 : forall (q1 q2 : Q_as_COrdField) (x : R1) (H : q1[<]q2), ((inj_Q R1 (q1[+](q2[-]q1) [/]ThreeNZ)[<]x) and (trichotomy x q1 q2[=]q1[+](q2[-]q1) [/]ThreeNZ)) or (x[<]inj_Q R1 (q2[-](q2[-]q1) [/]ThreeNZ)) and (trichotomy x q1 q2[=]q2[-](q2[-]q1) [/]ThreeNZ).
proof: Proof. intros. unfold trichotomy in |- *. elim (Qlt_eq_gt_dec' q1 q2). intro y. elim y. intro y0. simpl in |- *. apply cotrans_analyze_strong. intro. apply False_rect. generalize b. change (Not (q2[<]q1)) in |- *. apply less_antisymmetric_unfolded. assumption. intro. exfalso. generalize b. change (q1[~=]q2) in |- *. apply ap_imp_neq. apply less_imp_ap. assumption. Qed.
imports: CoRN.reals.Q_in_CReals