proposition: Lemma Qquadratic_Qpositive_to_Q_4 : forall (a b c d e f g h : Z) (p1 p2 : Qpositive) (H_Qquadratic_sg_denom_nonzero : Qquadratic_sg_denom_nonzero e f g h p1 p2), ~ same_ratio a b c d e f g h -> q_sign a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero = 0%Z -> Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero = Zero.
proof: Proof. intros a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero. functional induction (Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero); intros; try solve [ Falsum ]; trivial;Clear_eq_; match goal with [ id1 : q_sign ?a ?b ?c ?d ?e ?f ?g ?h ?p1 ?p2 ?H_Qquadratic_sg_denom_nonzero = _, id2 : q_sign ?a ?b ?c ?d ?e ?f ?g ?h ?p1 ?p2 ?H_Qquadratic_sg_denom_nonzero = _ |- _ ] => rewrite id1 in id2;discriminate id2 end. Qed.
imports: Coq(FunInd) QArithSternBrocot(homographic_correctness)