proposition: Lemma Q_tail_Qmult : forall x y : Q, x <> Zero -> y <> Zero -> Q_tail (Qmult x y) = Qpositive_mult (Q_tail x) (Q_tail y).
proof: Proof. intros [| px| px] [| py| py] Hx Hy; trivial; Falsum. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)