proposition: Lemma AM_Perp_AM_Perp_AM_Par : forall A B C D U V, C<>D -> AM_Perp A B C D -> AM_Perp U V C D -> AM_Par A B U V.
proof: Proof. intros A B C D U V. intros. destruct (eq_dec_points A B). subst. unfold AM_Par, twice_signed_area4. rewrite twice_signed_area_AAB. rewrite twice_signed_area_ABA. ring. assert (Perp A B C D) by (apply Perp_AM_Perp;auto). destruct (eq_dec_points U V). subst. unfold AM_Par, twice_signed_area4. rewrite twice_signed_area_perm. rewrite twice_signed_area_cyclic. ring. assert (Perp U V C D) by (apply Perp_AM_Perp;auto). assert (Par A B U V). apply par_perp2__par with C D C D;Par;Perp. apply Par_AM_Par;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