proposition: Lemma perp_triangle_area : forall A B C, A<>C -> AM_Per A B C -> twice_signed_area A B C * twice_signed_area A B C =F= square_dist A B * square_dist B C.
proof: Proof. intros A B C. rewrite Per_AM_Per. rewrite characterization_of_right_triangle_F. rewrite characterization_of_neq_F. unfold twice_signed_area, AM_Per, Py, square_dist, cross_product. decompose_coordinates;simpl. intros. put_negs_in_goal. express_disj_as_a_single_poly. nsatz. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems