proposition: Lemma Qhomographic_Qpositive_to_Q_0 : forall (a b c d : Z) (p : Qpositive) (H_Qhomographic_sg_denom_nonzero : Qhomographic_sg_denom_nonzero c d p) (Hc : c <> 0%Z), (a * d)%Z = (b * c)%Z -> d = 0%Z -> Qhomographic_Qpositive_to_Q a b c d p H_Qhomographic_sg_denom_nonzero = fraction_encoding a c Hc.
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 ]; unfold Qhomographic_Qpositive_to_Q in |- *. apply fraction_encoding_equal. apply fraction_encoding_equal. Defined.
imports: Coq(FunInd)