proposition: Lemma on : forall A B C D J, CI J A C D /\ OnCirc B J -> tarski_axioms.Cong A B C D.
proof: Proof. intros. unfold CI,OnCirc in *. destruct J. destruct p. spliter. congruence. 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