proposition: Lemma Col_AM_Col : forall A B C, AM_Col A B C <-> Col A B C.
proof: Proof. intros. unfold AM_Col. rewrite characterization_of_collinearity_F. unfold twice_signed_area, cross_product. decompose_coordinates. simpl. split. intros HEQ;rewrite <- HEQ;ring. intros HEQ;rewrite <- HEQ;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