proposition: Lemma Qquadratic_sg_denom_nonzero_Zero_Zero_always : forall (k g h : Z) (p1 p2 : Qpositive), k <> 0%Z -> (0 < g)%Z -> (0 < h)%Z -> Qquadratic_sg_denom_nonzero 0 0 (k * g) (k * h) p1 p2.
proof: Proof. intros k g h p1 p2 Hk Hg Hh. generalize g h Hg Hh p2. induction p1. intros. case p0. intro p3. apply Qquadratic_signok1. simpl in |- *. replace (k * g0 + k * h0)%Z with (k * (g0 + h0))%Z; [ apply IHp1; try first [ assumption | repeat apply Zlt_resp_pos ]; try assumption | abstract ring ]. intro p3. apply Qquadratic_signok2. simpl in |- *. replace (k * g0 + k * h0)%Z with (k * (g0 + h0))%Z; [ apply IHp1; try first [ assumption | repeat apply Zlt_resp_pos ]; try assumption | abstract ring ]. apply Qquadratic_signok0. reflexivity. simpl in |- *. apply Qhomographic_sg_denom_nonzero_Zero_always. replace (k * g0 + k * h0)%Z with (k * (g0 + h0))%Z. intro. apply Hk. apply Zmult_integral_l with (g0 + h0)%Z. apply sym_not_eq. apply Zorder.Zlt_not_eq. apply Zlt_resp_pos; assumption. assumption. abstract ring. intros. case p0. intro p3. apply Qquadratic_signok3. simpl in |- *. replace (k * g0 + k * h0)%Z with (k * (g0 + h0))%Z; [ apply Qquadratic_sg_denom_nonzero_always; try first [ assumption | repeat apply Zlt_resp_pos ]; try assumption | abstract ring ]. intro p3. apply Qquadratic_signok4. simpl in |- *. replace (k * g0 + k * h0)%Z with (k * (g0 + h0))%Z; [ apply Qquadratic_sg_denom_nonzero_always; try first [ assumption | repeat apply Zlt_resp_pos ]; try assumption | abstract ring ]. apply Qquadratic_signok0. reflexivity. simpl in |- *. apply Qhomographic_sg_denom_nonzero_Zero_always. replace (k * g0 + k * h0)%Z with (k * (g0 + h0))%Z. intro. apply Hk. apply Zmult_integral_l with (g0 + h0)%Z. apply sym_not_eq. apply Zorder.Zlt_not_eq. apply Zlt_resp_pos; assumption. assumption. abstract ring. intros. apply Qquadratic_signok0'. reflexivity. simpl in |- *. rewrite Z.mul_comm with k h0. rewrite Z.mul_comm with k g0. apply Qhomographic_sg_denom_nonzero_always_1; assumption. Defined.
imports: QArithSternBrocot(general_Q Zaux)