proposition: Lemma Qquadratic_sg_denom_nonzero_Zero_Zero_always_Zero : forall (g : Z) (p1 p2 : Qpositive), g <> 0%Z -> Qquadratic_sg_denom_nonzero 0 0 g 0 p1 p2.
proof: Proof. intros g p1 p2 Hg. generalize g Hg p2. abstract (induction p1; intros; [ destruct p0 as [q| q| ]; [ apply Qquadratic_signok1; simpl in |- *; rewrite Zplus_0_r; rewrite <- Zmult_1_r with g0; apply Qquadratic_sg_denom_nonzero_Zero_Zero_always | apply Qquadratic_signok2; simpl in |- *; rewrite Zplus_0_r; apply IHp1; assumption | apply Qquadratic_signok0 ] | destruct p0 as [q| q| ]; [ apply Qquadratic_signok3; simpl in |- *; rewrite Zplus_0_r; rewrite <- Zmult_1_r with g0; apply Qquadratic_sg_denom_nonzero_always | apply Qquadratic_signok4; simpl in |- *; rewrite Zplus_0_r; rewrite <- Zmult_1_r with g0; apply Qquadratic_sg_denom_nonzero_always_Zero_always_Zero | apply Qquadratic_signok0 ] | apply Qquadratic_signok0'; [ constructor | simpl in |- *; apply Qhomographic_sg_denom_nonzero_always_Zero; assumption ] ]; simpl in |- *; try rewrite Zplus_0_r; try apply Qhomographic_sg_denom_nonzero_Zero_always; assumption || (try constructor)). Defined.
imports: QArithSternBrocot(general_Q Zaux)