proposition: Lemma construct_intersection : forall A B C X1 X2 X3, ~ Col A B C -> Par A C B X1 -> Par A B C X2 -> Par B C A X3 -> exists E, Col E A X3 /\ Col E B X1.
proof: Proof. intros A B C X1 X2 X3 HNC HPar1 HPar2 HPar3. apply cop_npar__inter_exists. CopR. intro HNPar; apply HNC. assert (HFalsePar : Par B C A C) by (apply (par_trans B C B X1 A C); finish; apply (par_trans B C A X3 B); finish). perm_apply (par_id C B A). Qed.
imports: GeoCoq.Highschool.circumcenter