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