fact: Definition AM_CongAL A B C D E F := Py A B C * twice_signed_area D E F =F= Py D E F * twice_signed_area A B C.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems