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