proposition: Theorem new_equality : (3 * p - 4 * q) * (3 * p - 4 * q) = 2 * ((3 * q - 2 * p) * (3 * q - 2 * p)).
proof: Proof. repeat rewrite sub_square_identity; auto with arith. repeat rewrite square_recompose; rewrite mult_minus_distr_l. apply minus_eq_decompose; try rewrite hyp_sqrt; ring. Qed.
imports: Coq(ArithRing) Coq(Compare_dec) Coq(Wf_nat) Coq(Arith) Coq(Lia)