proposition: Lemma Q_tail_Q_neg : forall q : Q, Qlt q Zero -> q = Qneg (Q_tail q).
proof: Proof. intros [| q| q]; unfold Qlt in |- *; intros H; inversion H || unfold Q_tail in |- *; reflexivity. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)