proposition: Lemma Per_AM_Per : forall A B C, AM_Per A B C <-> Per A B C.
proof: Proof. intros. split; rewrite (characterization_of_right_triangle_F); unfold AM_Per, Py, square_dist; decompose_coordinates; intro; assert (NU : ~ (- (2) =F= 0)) by prove_discr_for_powers_of_2; 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