proposition: Lemma Qhomographic_sg_denom_nonzero_Zero_always : forall (d : Z) (p : Qpositive), d <> 0%Z -> Qhomographic_sg_denom_nonzero 0 d p.
proof: Proof. intros. induction p. apply Qhomographic_signok1. simpl in |- *. assumption. apply Qhomographic_signok2. simpl in |- *. replace d with (1 * d)%Z. apply Qhomographic_sg_denom_nonzero_always_1. assumption. constructor. constructor. rewrite Zmult_1_l. reflexivity. apply Qhomographic_signok0. reflexivity. simpl in |- *. assumption. Defined.
imports: Coq(ZArithRing)