proposition: Lemma project_not_id : forall A B X Y P P', Proj P P' A B X Y -> ~Col A B P -> P <> P'.
proof: Proof. intros. intro. apply H0. subst P'. unfold Proj in H. spliter. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors