proposition: Lemma shrink23 : forall q1 q2 : Q_as_COrdField, (q1[<]q2) -> q1[+](q2[-]q1) [/]ThreeNZ[<]q2[-](q2[-]q1) [/]ThreeNZ.
proof: Proof. intros. apply plus_cancel_less with (R := Q_as_COrdField) (z := (q2[-]q1) [/]ThreeNZ). rstepl (q2[-](q2[-]q1) [/]ThreeNZ). rstepr q2. apply plus_cancel_less with (R := Q_as_COrdField) (z := [--]q2). rstepr [--]([0]:Q_as_COrdField). rstepl [--]((q2[-]q1) [/]ThreeNZ). apply inv_resp_less. apply mult_cancel_less with (R := Q_as_COrdField) (z := Three:Q_as_COrdField). apply pos_nring_S. rstepl ([0]:Q_as_COrdField). rstepr (q2[-]q1). apply shift_zero_less_minus. assumption. Qed.
imports: CoRN.reals.Q_in_CReals