proposition: Lemma Qquadratic_sg_denom_nonzero_Zero_always_Zero_always : forall (k f h : Z) (p1 p2 : Qpositive), k <> 0%Z -> (0 < f)%Z -> (0 < h)%Z -> Qquadratic_sg_denom_nonzero 0 (k * f) 0 (k * h) p1 p2.
proof: Proof. intros k f h p1 p2 Hk Hf Hh. generalize f h Hf Hh p2. abstract (induction p1; intros; [ destruct p0 as [q| q| ]; [ apply Qquadratic_signok1; simpl in |- *; rewrite Zplus_0_r; rewrite <- Zmult_plus_distr_r with k f0 h0; apply IHp1 | apply Qquadratic_signok2; simpl in |- *; rewrite Zplus_0_r; rewrite <- Zmult_plus_distr_r with k f0 h0; apply Qquadratic_sg_denom_nonzero_always | apply Qquadratic_signok0; [ reflexivity | simpl in |- *; rewrite Z.mul_comm; rewrite Z.mul_comm with k h0; apply Qhomographic_sg_denom_nonzero_always_1 ] ] | destruct p0 as [q| q| ]; [ apply Qquadratic_signok3; simpl in |- *; rewrite Zplus_0_r; rewrite <- Zmult_plus_distr_r with k f0 h0; apply IHp1 | apply Qquadratic_signok4; simpl in |- *; rewrite Zplus_0_r; rewrite <- Zmult_plus_distr_r with k f0 h0; apply Qquadratic_sg_denom_nonzero_always | apply Qquadratic_signok0; [ reflexivity | simpl in |- *; rewrite Z.mul_comm; rewrite Z.mul_comm with k h0; apply Qhomographic_sg_denom_nonzero_always_1 ] ] | apply Qquadratic_signok0'; [ reflexivity | simpl in |- *; rewrite <- Zmult_plus_distr_r with k f0 h0; apply Qhomographic_sg_denom_nonzero_Zero_always; apply Zmult_resp_nonzero; [ idtac | apply sym_not_eq; apply Zorder.Zlt_not_eq; apply Zlt_resp_pos ] ] ]; try first [ assumption | repeat apply Zlt_resp_pos ]; assumption). Defined.
imports: QArithSternBrocot(general_Q Zaux)