proposition: Lemma Qpos_not_lt_Qneg : forall x y, ~ Qlt (Qpos y) (Qneg x).
proof: Proof. intros x y Hc; apply (Qlt_irreflexive (Qneg x)); apply Qlt_transitive with (Qpos y); trivial. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)