proposition: Lemma inside : forall A B C J P, CI J C A B /\ InCirc P J <-> exists X Y, CI J C A B /\ Definitions.BetS X C Y /\ tarski_axioms.Cong C Y A B /\ tarski_axioms.Cong C X A B /\ Definitions.BetS X P Y.
proof: Proof. intros. unfold InCirc, CI. destruct J;destruct p. split. intros;spliter. decompose [ex and] H0;clear H0. exists x. exists x0. inversion H; subst; auto. intros. decompose [ex and] H;clear H. inversion H1; subst;split; auto. exists x; exists x0;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