proposition: Lemma shrink23d : forall r1 r2 : R1, r1[<]r2 -> r1[+](r2[-]r1) [/]ThreeNZ[<]r2[-](r2[-]r1) [/]ThreeNZ.
proof: Proof. intros. apply plus_cancel_less with (z := (r2[-]r1) [/]ThreeNZ). rstepl (r2[-](r2[-]r1) [/]ThreeNZ). rstepr r2. apply plus_cancel_less with (z := [--]r2). rstepr ([--]([0]:R1)). rstepl ([--]((r2[-]r1) [/]ThreeNZ)). apply inv_resp_less. apply mult_cancel_less with (z := Three:R1). apply pos_nring_S. rstepl ([0]:R1). rstepr (r2[-]r1). apply shift_zero_less_minus. assumption. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon