proposition: Lemma exists_projp : forall A B P, A <> B -> exists P', Projp P P' A B.
proof: Proof. intros A B P HAB. elim (col_dec A B P); intro HNC; [exists P; split; Col; right|]. destruct (l8_18_existence A B P HNC) as [P' HP']. exists P'; split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths