proposition: Lemma shrink24 : forall q1 q2 : Q_as_COrdField, (q1[<]q2) -> q1[+](q2[-]q1) [/]ThreeNZ[<]q2.
proof: Proof. intros. apply less_transitive_unfolded with (q2[-](q2[-]q1) [/]ThreeNZ). apply shrink23. assumption. astepl (q2[+][--]((q2[-]q1) [/]ThreeNZ)). astepr (q2[+][0]). apply plus_resp_less_lft. apply inv_cancel_less. rstepl ([0]:Q_as_COrdField). rstepr ((q2[-]q1) [/]ThreeNZ). apply div_resp_pos. apply pos_three. apply shift_zero_less_minus. assumption. Qed.
imports: CoRN.reals.Q_in_CReals