proposition: Lemma Qlt_Zero_Qminus : forall x y : Q, Qlt Zero (Qminus y x) -> Qlt x y.
proof: Proof. intros x y H; replace x with (Qplus x Zero); [ idtac | ring ]; replace y with (Qplus x (Qminus y x)); [ idtac | ring ]; unfold Qlt in |- *; apply Qgt_plus; assumption. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)