fact: Definition AM_on_foot Y P U V := AM_Perp Y P U V /\ AM_Col Y U V /\ U <> V.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems