proposition: Lemma AM_Perp_triv2 : forall A B C, AM_Perp A A B C.
proof: Proof. intros. unfold AM_Perp, Py4. ring. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems