proposition: Lemma Perp_AM_Perp : forall A B C D, (AM_Perp A B C D /\ A <> B /\ C <> D) <-> Perp A B C D.
proof: Proof. intros. rewrite (characterization_of_perpendicularity_F). repeat (rewrite characterization_of_neq_F). unfold AM_Perp, Py4, Py, square_dist. decompose_coordinates. split;intro. use H; repeat split; try assumption. assert (NU : ~ (- (2) =F= 0)) by prove_discr_for_powers_of_2. nsatz. use H;repeat split;try assumption. 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