proposition: Lemma InCirc_not_OnCirc: forall J A, InCirc J A -> ~ OnCirc J A.
proof: Proof. unfold InCirc, OnCirc in *. intros A J. destruct J as [[X C] D]. intros. destruct H as [U [V HUV]];spliter. intro. unfold Definitions.BetS in *;spliter. assert (tarski_axioms.Cong X U X V) by CongR. assert (Midpoint X U V) by (split;Cong). assert (Midpoint X A V). apply (cong_col_mid A X V). assumption. ColR. CongR. treat_equalities;intuition. 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