proposition: Lemma Qsgn_34:forall x:Q, Qsgn x <> (-1)%Z -> Qle Zero x.
proof: Proof. intros [|x|x] Hx; auto; try apply Qle_reflexive; apply False_ind; apply Hx; reflexivity. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)