proposition: Lemma dcotrans_analyze_strong : forall (r1 r2 : R1) (H : r1[<]r2), {s : R1 | A s | r1[+](r2[-]r1) [/]ThreeNZ[<]s} and dcotrans_analyze r1 r2 H[=]r1[+](r2[-]r1) [/]ThreeNZ or is_upper_bound R1 A (r2[-](r2[-]r1) [/]ThreeNZ) and dcotrans_analyze r1 r2 H[=]r2[-](r2[-]r1) [/]ThreeNZ.
proof: Proof. intros. unfold dcotrans_analyze in |- *. elim (located (r1[+](r2[-]r1) [/]ThreeNZ) (r2[-](r2[-]r1) [/]ThreeNZ) (shrink23d _ _ H)). intro. right. split. assumption. apply eq_reflexive_unfolded. intro. left. split. assumption. apply eq_reflexive_unfolded. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon