proposition: Lemma Qpos_lt_plus : forall (a b:Q), a< b -> {c:Qpos | b==(a+c)}.
proof: Proof. intros. assert (0<b-a). apply: shift_zero_less_minus. assumption. exists (mkQpos H0). QposRing. Defined.
imports: Coq.QArith.QArith Coq.QArith.Qpower CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 Coq.Logic.Eqdep_dec CoRN.tactics.CornTac Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.Q