proposition: Lemma projp_col : forall A B P P', Projp P P' A B -> Col A B P'.
proof: Proof. intros A B P P' H; destruct H as [H' H]; clear H'. induction H; spliter; treat_equalities; Col. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors