proposition: Lemma dif_cotrans_strong : forall I1 : Real_Interval, {s : R1 | A s | fstT I1[+](sndT I1[-]fstT I1) [/]ThreeNZ[<]s} and dif_cotrans I1 = Build_Interval _ (fstT I1[+](sndT I1[-]fstT I1) [/]ThreeNZ, sndT I1) (shrink24d (fstT I1) (sndT I1) (is_interval _ I1)) or is_upper_bound R1 A (sndT I1[-](sndT I1[-]fstT I1) [/]ThreeNZ) and dif_cotrans I1 = Build_Interval _ (fstT I1, sndT I1[-](sndT I1[-]fstT I1) [/]ThreeNZ) (shrink13d (fstT I1) (sndT I1) (is_interval _ I1)).
proof: Proof. intros. case I1. intros i pi. elim (dcotrans_analyze_strong _ _ pi). intro y. left. elim y. intros H H0. split. exact H. cut (dif_cotrans (Build_Interval _ i pi) = Build_Interval _ (fstT i[+](sndT i[-]fstT i) [/]ThreeNZ, sndT i) (shrink24d (fstT i) (sndT i) pi)). intro H1. rewrite H1. simpl in |- *. apply refl_equal. unfold dif_cotrans in |- *. apply not_r_cor_rect. apply or_not_and. right. apply ap_imp_neq. astepl (fstT i[+](sndT i[-]fstT i) [/]ThreeNZ). apply less_imp_ap. apply shrink23d. assumption. intro y. elim y. intros H H0. right. split. exact H. cut (dif_cotrans (Build_Interval R1 i pi) = Build_Interval R1 (fstT i, sndT i[-](sndT i[-]fstT i) [/]ThreeNZ) (shrink13d (fstT i) (sndT i) pi)). intro. rewrite H1. simpl in |- *. reflexivity. unfold dif_cotrans in |- *. apply not_l_cor_rect. apply or_not_and. right. apply ap_imp_neq. astepl (sndT i[-](sndT i[-]fstT i) [/]ThreeNZ). apply Greater_imp_ap. apply shrink23d. assumption. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon