proposition: Lemma col_per2__per : forall A B C P X, A <> B -> Col A B C -> Per A X P -> Per B X P -> Per C X P.
proof: Proof. intros. destruct (symmetric_point_construction P X) as [Q]. exists Q; split. assumption. apply (l4_17 A B); try apply per_double_cong with X; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR