proposition: Lemma ratio_zero : forall A B C D, C<>D -> AM_Par A B C D -> (ratio A B C D =F= 0 -> A = B).
proof: Proof. intros A B C D. rewrite characterization_of_neq_F. rewrite characterization_of_equality_F. unfold AM_Par, ratio, twice_signed_area4, twice_signed_area, scalar_product, cross_product . decompose_coordinates;simpl. intros. apply (field_prop_zero) in H1. split. put_negs_in_goal. express_disj_as_a_single_poly. nsatz. put_negs_in_goal. express_disj_as_a_single_poly. nsatz. intro. apply H. rewrite <- H2. ring. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems