proposition: Lemma Cong_AM_Cong: forall A B C D, AM_Cong A B C D <-> Cong A B C D.
proof: Proof. intros. rewrite characterization_of_congruence_F. unfold AM_Cong, Py, square_dist. decompose_coordinates. split;intro; 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