proposition: Lemma AM_Par_ratio_AM_Par : forall P Q C D, AM_Par P Q C D -> ratio P Q C D =F= 1 -> C<>D -> AM_Par D Q P C.
proof: Proof. intros P Q C D H1 H2 H3. setoid_rewrite characterization_of_neq_F in H3. unfold AM_Par, twice_signed_area4, twice_signed_area, ratio in *. decompose_coordinates. unfold cross_product, scalar_product in *;simpl in *. assert (((Qx - Px) * (Dx - Cx) + (Qy - Py0) * (Dy - Cy)) =F= ((Dx - Cx) * (Dx - Cx) + (Dy - Cy) * (Dy - Cy))). assert (((Qx - Px) * (Dx - Cx) + (Qy - Py0) * (Dy - Cy)) / ((Dx - Cx) * (Dx - Cx) + (Dy - Cy) * (Dy - Cy)) * ((Dx - Cx) * (Dx - Cx) + (Dy - Cy) * (Dy - Cy)) =F= ((Dx - Cx) * (Dx - Cx) + (Dy - Cy) * (Dy - Cy))). rewrite H2. ring. rewrite <- H. field. intro. rewrite <- H0 in H3. apply H3;ring. put_negs_in_goal. express_disj_as_a_single_poly. clear H2. 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