proposition: Lemma tcp a b c : ~ colI a b c -> exists x, cong a x b x /\ cong a x c x /\ cop a b c x.
proof: Proof. cut (triangle_circumscription_principle); [|have: tarski_s_parallel_postulate]. move=> HP HNC1; destruct (HP a b c) as [x [HC1 [HC2 HCop]]]; [|exists x]. by move: HNC1; rewrite /Col /colI; intuition. split; [|split]; [intuition..|move: HCop; rewrite -Cop__Coplanar]. move => [e [f [g [HNC2 [[iaP aP] [[ibP bP] [[icP cP] [ixP xP]]]]]]]]. exists e, f, g; split; first by rewrite /Col /colI; intuition. split; first by exists iaP; move: aP; rewrite /Col /colI; intuition. split; first by exists ibP; move: bP; rewrite /Col /colI; intuition. split; first by exists icP; move: cP; rewrite /Col /colI; intuition. by exists ixP; move: xP; rewrite /Col /colI; intuition. by unfold tarski_s_parallel_postulate; apply euclidT. apply equivalent_postulates_without_decidability_of_intersection_of_lines_bis; simpl; tauto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype seq order) mathcomp(fintype bigop) mathcomp(ssralg ssrnum matrix) mathcomp(zmodp) GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.gupta_inspired_to_tarski GeoCoq.Meta_theory.Counter_models.coplanarity GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Tarski_dev.Ch12_parallel_inter_dec