proposition: Lemma Q_tail_Qplus_pos : forall x y : Q, Qlt Zero x -> Qlt Zero y -> Q_tail (Qplus x y) = Qpositive_plus (Q_tail x) (Q_tail y).
proof: Proof. intros [| px| px] [| py| py] Hx Hy; trivial; solve [ inversion Hx | inversion Hy ]. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)