proposition: Lemma inv_exists_with_notation : forall A, Col O E A -> exists B, inv O E E' A B.
proof: Proof. intros; induction (eq_dec_points A O); [subst; exists O; right; auto|]. destruct (inv_exists O E E' A) as [IA HIA]; try (exists IA; left); auto. apply 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