proposition: Lemma perp_in2__col : forall A B A' B' X Y P, Perp_at P A B X Y -> Perp_at P A' B' X Y -> Col A B A'.
proof: Proof. intros A B A' B' X Y P. apply cop4_perp_in2__col; apply all_coplanar. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel