proposition: Lemma Qquadratic_sg_denom_nonzero_always_Zero_always_Zero : forall (k e g : Z) (p1 p2 : Qpositive), k <> 0%Z -> (0 < e)%Z -> (0 < g)%Z -> Qquadratic_sg_denom_nonzero (k * e) 0 (k * g) 0 p1 p2.
proof: Proof. intros k e g p1 p2 Hk He Hg. generalize e g He Hg p2. abstract (induction p1; intros; [ destruct p0 as [q| q| ]; [ apply Qquadratic_signok1; simpl in |- *; repeat rewrite Zplus_0_r; rewrite <- Zmult_plus_distr_r with k e0 g0; apply Qquadratic_sg_denom_nonzero_always | apply Qquadratic_signok2; simpl in |- *; repeat rewrite Zplus_0_r; rewrite <- Zmult_plus_distr_r with k e0 g0; apply IHp1 | apply Qquadratic_signok0; [ reflexivity | repeat rewrite Zplus_0_r; rewrite Z.mul_comm; rewrite Z.mul_comm with k g0; apply Qhomographic_sg_denom_nonzero_always_1 ] ] | destruct p0 as [q| q| ]; [ apply Qquadratic_signok3; simpl in |- *; repeat rewrite Zplus_0_r; rewrite <- Zmult_plus_distr_r with k e0 g0; apply Qquadratic_sg_denom_nonzero_always | apply Qquadratic_signok4; simpl in |- *; repeat rewrite Zplus_0_r; rewrite <- Zmult_plus_distr_r with k e0 g0; apply IHp1 | apply Qquadratic_signok0; [ reflexivity | repeat rewrite Zplus_0_r; rewrite Z.mul_comm; rewrite Z.mul_comm with k g0; apply Qhomographic_sg_denom_nonzero_always_1 ] ] | apply Qquadratic_signok0'; [ reflexivity | simpl in |- *; rewrite <- Zmult_plus_distr_r with k e0 g0; apply Qhomographic_sg_denom_nonzero_always_Zero; apply Zmult_resp_nonzero; [ idtac | apply sym_not_eq; apply Zorder.Zlt_not_eq; apply Zlt_resp_pos ] ] ]; assumption || (try apply Zlt_resp_pos); assumption). Defined.
imports: QArithSternBrocot(general_Q Zaux)