proposition: Lemma Qhomographic_sg_denom_nonzero_always_1 : forall (d k k' : Z) (p : Qpositive), d <> 0%Z -> (0 < k)%Z -> (0 < k')%Z -> Qhomographic_sg_denom_nonzero (k * d) (k' * d) p.
proof: Proof. intros. generalize k k' H0 H1. induction p. intros. apply Qhomographic_signok1. replace (k0 * d + k'0 * d)%Z with ((k0 + k'0) * d)%Z. apply IHp. assumption. replace 0%Z with (0 + 0)%Z. apply Zlt_plus_plus. assumption. assumption. constructor. rewrite Zmult_plus_distr_l; reflexivity. intros. apply Qhomographic_signok2. replace (k0 * d + k'0 * d)%Z with ((k0 + k'0) * d)%Z. apply IHp. replace 0%Z with (0 + 0)%Z. apply Zlt_plus_plus. assumption. assumption. constructor. assumption. rewrite Zmult_plus_distr_l; reflexivity. intros. apply Qhomographic_signok0. reflexivity. replace (k0 * d + k'0 * d)%Z with ((k0 + k'0) * d)%Z. intro. apply H. apply Zmult_integral_l with (k0 + k'0)%Z. apply Zgt_not_eq. apply Z.lt_gt. replace 0%Z with (0 + 0)%Z. apply Zlt_plus_plus. assumption. assumption. constructor. rewrite Z.mul_comm. assumption. rewrite Zmult_plus_distr_l; reflexivity. Defined.
imports: Coq(ZArithRing)