proposition: Lemma col_projp_eq : forall A B P P', Col A B P -> Projp P P' A B -> P = P'.
proof: Proof. intros A B P P' HCol1 HProjp. destruct HProjp as [HDiff HProjp]; elim HProjp; clear HProjp; intro HProjp; [exfalso; destruct HProjp as [HCol2 HPerp]|spliter; auto]. apply perp_not_col2 in HPerp; induction HPerp; intuition. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors