proposition: Lemma InCirc_InCirc : forall A K, euclidean_axioms.InCirc A K -> InCirc A K.
proof: Proof. intros. unfold euclidean_axioms.InCirc in *. destruct K as [[C U] V]. unfold euclidean_axioms.InCirc in *. destruct H as [X [Y [C0 [V [W [HW1 HW2]]]]]]. destruct HW2. - unfold eq in *;subst. unfold euclidean_axioms.CI in *;simpl in *. unfold CI in *. spliter. inversion H;subst. destruct (eq_dec_points C0 V). subst. destruct (symmetric_point_construction W V) as [X0 HX]. exists X0. exists W. assert_bets. assert_diffs. split. unfold Definitions.BetS;Between. split;Cong. split;Cong. unfold Definitions.BetS;Between. destruct (segment_construction_3 C0 V V W H1 H0) as [X0 [HX0 HX1]]. destruct (symmetric_point_construction X0 C0) as [Y0 HY0]. exists X0. exists Y0. assert_bets. assert_diffs. unfold Definitions.BetS;split;auto. split. apply cong_transitivity with C0 X0; Cong. split. auto. split;auto. - spliter. unfold euclidean_axioms.CI in *;simpl in *;unfold CI in *;spliter. inversion H2;subst. assert (C0 <> A). { intro;treat_equalities. unfold Definitions.BetS in *;intuition. } destruct (segment_construction_3 C0 A V W H4 H3) as [X0 [HX0 HX1]]. assert (A <> X0). { intro. subst. assert (HCong: tarski_axioms.Cong C0 Y C0 X) by CongR. unfold Definitions.BetS in *;spliter. assert (eq:= between_cong C0 X Y H HCong). contradiction. } destruct (symmetric_point_construction X0 C0) as [Y0 HY0]. assert (A <> Y0). { intro. subst. unfold Definitions.BetS in *;spliter. assert (HCong: tarski_axioms.Cong C0 Y C0 X) by CongR. assert (eq:= between_cong C0 X Y H HCong). contradiction. } destruct HX0 as [HA [ HB [HC | HC]]]. exists X0. exists Y0. assert_diffs. split;unfold Definitions.BetS;Between. split. apply cong_transitivity with C0 X0; Cong. split. Cong. split;auto. assert_bets; eBetween. assert (Lt C0 Y C0 X) by (unfold Definitions.BetS in *;spliter;apply (bet__lt1213);auto). assert (Le C0 X0 C0 A) by (apply (bet__le1213);auto). assert (HCong: tarski_axioms.Cong C0 X0 C0 X) by CongR. assert (Lt C0 X C0 A) by (apply (cong2_lt__lt C0 X0 C0 A);finish). assert (Lt C0 Y C0 A) by (apply (le3456_lt__lt) with C0 X;auto using lt__le). assert (Hc : tarski_axioms.Cong C0 Y C0 A) by Cong. apply cong__nlt in Hc. 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