proposition: Lemma Qquadratic_Qpositive_to_Q_7 : 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 = (-1)%Z -> Z.sgn (qnew_a a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero + qnew_b a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero + qnew_c a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero + qnew_d a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) = 1%Z -> forall hyp_quadraticAcc : quadraticAcc (qnew_a a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (qnew_b a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (qnew_c a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (qnew_d a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (- qnew_e a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (- qnew_f a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (- qnew_g a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (- qnew_h a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (qnew_p1 a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (qnew_p2 a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero), Qquadratic_Qpositive_to_Q a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero = Qneg (Qquadratic_Qpositive_to_Qpositive (qnew_a a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (qnew_b a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (qnew_c a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (qnew_d a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (- qnew_e a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (- qnew_f a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (- qnew_g a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (- qnew_h a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (qnew_p1 a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) (qnew_p2 a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero) hyp_quadraticAcc).
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_; QSign_mismatch_ || apply f_equal with Qpositive; apply Qquadratic_Qpositive_to_Qpositive_equal. Qed.
imports: Coq(FunInd) QArithSternBrocot(homographic_correctness)