proposition: Lemma eOutCirc_OutCirc : forall A K, euclidean_axioms.OutCirc A K -> OutCirc A K.
proof: Proof. intros. destruct K. destruct p. unfold euclidean_axioms.OutCirc in *. destruct H as [X [Y [U [V HV]]]]. spliter. unfold euclidean_axioms.CI in *;simpl in *;unfold CI in *. spliter. inversion H;subst. exists X;auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Axioms.euclidean_axioms GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates