proposition: Lemma AM_perp_AM_Par_AM_perp : forall A B C D U V, A<>B -> AM_Perp A B C D -> AM_Par A B U V -> AM_Perp U V C D.
proof: Proof. intros A B C D U V. intros. destruct (eq_dec_points C D). subst. apply AM_Perp_triv1. destruct (eq_dec_points U V). subst. apply AM_Perp_triv2. assert (Perp A B C D) by (apply Perp_AM_Perp;auto). assert (Par A B U V) by (apply Par_AM_Par;auto). assert (Perp U V C D). apply par_perp__perp with A B;auto. apply Perp_AM_Perp;auto. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems