proposition: Lemma triangle_area : forall A B C H, AM_on_foot H A B C -> twice_signed_area A B C * twice_signed_area A B C =F= square_dist A H * square_dist B C.
proof: Proof. intros A B C H. unfold AM_on_foot, AM_Col, AM_Perp, Py4, Py, square_dist, twice_signed_area, cross_product. rewrite characterization_of_neq_F. decompose_coordinates;simpl. intros. use H0. put_negs_in_goal. express_disj_as_a_single_poly. assert (NU := neq20). 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