proposition: Lemma Par_AM_Par : forall A B C D, (A <> B /\ C <> D /\ AM_Par A B C D) <-> Par A B C D.
proof: Proof. intros. unfold AM_Par, twice_signed_area4, twice_signed_area. rewrite characterization_of_parallelism_F. rewrite characterization_of_neq_F. rewrite characterization_of_neq_F. decompose_coordinates. unfold cross_product;simpl. split. intros. use H. split;auto. nsatz. intros. use H. split;auto. split;auto. 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