proposition: Lemma triangle_circumscription : forall A B C, ~ Col A B C -> exists CC : Tpoint, Cong A CC B CC /\ Cong A CC C CC /\ Coplanar A B C CC.
proof: Proof. apply postulates_in_euclidean_context; simpl; repeat (try (left; reflexivity); right). Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec