proposition: Lemma InCircCenter: forall U V W, V<>W -> InCirc U (U, V, W).
proof: Proof. intros. unfold InCirc. destruct (eq_dec_points U V). subst. exists W. destruct (symmetric_point_construction W V) as [Y HY]. exists Y. assert_diffs. unfold Definitions.BetS. repeat split;Between;Cong. destruct (segment_construction_3 U V V W H0 H) as [X HX]. destruct (symmetric_point_construction X U) as [Y HY]. spliter. assert_diffs. assert_bets. exists X. exists Y. split. unfold Definitions.BetS;auto. split. apply cong_transitivity with U X; Cong. split. Cong. unfold Definitions.BetS;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