proposition: Lemma Qquadratic_00 : forall e f g h : Z, Qquadratic_denom_nonzero e f g h Zero Zero -> h <> 0%Z.
proof: Proof. intros. abstract (inversion H; assumption || (repeat match goal with | id1:(?X1 = ?X2) |- ?X3 => try discriminate id1; clear id1 end)). Defined.
imports: QArithSternBrocot(general_Q Zaux)