proposition: Lemma AM_lower_dim : exists A B C, ~ AM_Col A B C.
proof: Proof. exists O. exists E. exists E'. rewrite Col_AM_Col;auto using ncolOEE'. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems