proposition: Lemma qnew_c_equal : forall (a b c d e f g h : Z) (p1 p2 : Qpositive) (H_Qquadratic_sg_denom_nonzero1 H_Qquadratic_sg_denom_nonzero2 : Qquadratic_sg_denom_nonzero e f g h p1 p2), qnew_c a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero1 = qnew_c a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero2.
proof: Proof. intros a b c d e f g h p1 p2 H_Qquadratic_sg_denom_nonzero1 H_Qquadratic_sg_denom_nonzero2; unfold qnew_c in |- *; apply f_equal with (Z * Z)%type; apply f_equal with (Z * (Z * Z))%type; apply f_equal with (Z * (Z * (Z * Z)))%type; apply f_equal with (Z * (Z * (Z * Z)) * (Z * (Z * (Z * Z))))%type; apply f_equal with (Z * (Z * (Z * Z)) * (Z * (Z * (Z * Z))) * (Qpositive * Qpositive))%type; apply f_equal with (Z * (Z * (Z * (Z * Z)) * (Z * (Z * (Z * Z))) * (Qpositive * Qpositive)))%type; apply Qquadratic_sign_equal. Qed.
imports: Coq(FunInd) QArithSternBrocot(homographic_correctness)