proposition: Lemma Qhomographic_Qpositive_to_Q_2 : forall (a b c d : Z) (p : Qpositive) (H_Qhomographic_sg_denom_nonzero : Qhomographic_sg_denom_nonzero c d p), (a * d)%Z <> (b * c)%Z -> h_sign a b c d p H_Qhomographic_sg_denom_nonzero = 0%Z -> Qhomographic_Qpositive_to_Q a b c d p H_Qhomographic_sg_denom_nonzero = Zero.
proof: Proof. intros a b c d p H_Qhomographic_sg_denom_nonzero. functional induction (Qhomographic_Qpositive_to_Q a b c d p H_Qhomographic_sg_denom_nonzero);intros; try solve [Falsum|Sign_mismatch]; reflexivity. Qed.
imports: Coq(FunInd)