proposition: Lemma OnCirc_OnCirc : forall A P Q R, Q<>R -> OnCirc A (P,Q,R) -> euclidean_axioms.OnCirc A (P,Q,R).
proof: Proof. intros. unfold OnCirc in *. unfold euclidean_axioms.OnCirc. exists Q. exists R. exists P. unfold euclidean_axioms.CI;simpl;unfold CI. 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