proposition: Lemma shrink24d : forall r1 r2 : R1, r1[<]r2 -> r1[+](r2[-]r1) [/]ThreeNZ[<]r2.
proof: Proof. intros. apply less_transitive_unfolded with (y := r2[-](r2[-]r1) [/]ThreeNZ). apply shrink23d. assumption. astepl (r2[+][--]((r2[-]r1) [/]ThreeNZ)). astepr (r2[+][0]). apply plus_resp_less_lft. apply inv_cancel_less. rstepl ([0]:R1). rstepr ((r2[-]r1) [/]ThreeNZ). apply div_resp_pos. apply pos_three. apply shift_zero_less_minus. assumption. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon