proposition: Lemma if_cotrans_strong : forall (x : R1) (I1 : Rat_Interval), ((inj_Q R1 (fstT I1[+](sndT I1[-]fstT I1) [/]ThreeNZ)[<]x) and if_cotrans x I1 = Build_Interval _ (fstT I1[+](sndT I1[-]fstT I1) [/]ThreeNZ, sndT I1) (shrink24 (fstT I1) (sndT I1) (is_interval _ I1))) or (x[<]inj_Q R1 (sndT I1[-](sndT I1[-]fstT I1) [/]ThreeNZ)) and if_cotrans x I1 = Build_Interval _ (fstT I1, sndT I1[-](sndT I1[-]fstT I1) [/]ThreeNZ) (shrink13 (fstT I1) (sndT I1) (is_interval _ I1)).
proof: Proof. intros. case I1. intros i pi. elim (trichotomy_strong1 (fstT i) (sndT i) x pi). intro y. elim y. intros H H0. left. split. exact H. cut (if_cotrans x (Build_Interval Q_as_COrdField i pi) = Build_Interval Q_as_COrdField (fstT i[+](sndT i[-]fstT i) [/]ThreeNZ, sndT i) (shrink24 (fstT i) (sndT i) pi)). intro H1. rewrite H1. simpl in |- *. reflexivity. unfold if_cotrans in |- *. apply not_r_cor_rect. apply or_not_and. right. change (trichotomy x (fstT i) (sndT i)[~=]sndT i[-](sndT i[-]fstT i) [/]ThreeNZ) in |- *. apply ap_imp_neq. astepl (fstT i[+](sndT i[-]fstT i) [/]ThreeNZ). apply less_imp_ap. apply shrink23. assumption. intro. elim b. intros H H0. right. split. exact H. cut (if_cotrans x (Build_Interval Q_as_COrdField i pi) = Build_Interval Q_as_COrdField (fstT i, sndT i[-](sndT i[-]fstT i) [/]ThreeNZ) (shrink13 (fstT i) (sndT i) pi)). intro H1. rewrite H1. simpl in |- *. reflexivity. unfold if_cotrans in |- *. apply not_l_cor_rect. apply or_not_and. right. change (trichotomy x (fstT i) (sndT i)[~=] (fstT i)[+]((sndT i[-]fstT i) [/]ThreeNZ)) in |- *. apply ap_imp_neq. astepl (sndT i[-](sndT i[-]fstT i) [/]ThreeNZ). apply Greater_imp_ap. apply shrink23. assumption. Qed.
imports: CoRN.reals.Q_in_CReals