proposition: Lemma projp2_col : forall A B C P Q, Projp P A B C -> Projp Q A B C -> Col A P Q.
proof: Proof. intros A B C P Q H1 H2. destruct H1 as [H1 H3]; destruct H2 as [H2 H4]; induction H3; induction H4; spliter; treat_equalities; Col. apply perp2__col with B C; Perp. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors