proposition: Lemma bet_b1d1c A B B' C D D' T X : Bet A B X -> Bet A B' X -> Bet B D C -> Bet A D T -> Bet A D' T -> B <> D -> D <> C -> ~ Definitions.Col A B C -> Cong X T B' C -> Cong X B A B' -> Cong A C B T -> CongA A X T A B' D' -> Bet B' D' C.
proof: Proof. intros Hb1 Hb2 Hb3 Hb4 Hb5 HBD HDC HNC Hc1 Hc2 Hc3 HConga1. assert (HAT : A <> T) by (intro; treat_equalities; apply HNC; Col). assert (HC : Definitions.Col B' D' C). { assert (Out B' D' C); [|assert_cols; auto]. assert (HConga2 : CongA A X T A B' C). { apply l11_10 with B T A C; try apply out_trivial; try apply l6_6, bet_out; try solve [assert_diffs; auto]; Between. apply cong3_conga; try solve [assert_diffs; auto]; split; Cong; split ; Cong. } assert (HOS1 : OS B' A D' D). { apply invert_one_side, out_one_side; try (right; intro; apply HNC; assert_diffs; ColR). apply bet2_out_out with T T; try solve [assert_diffs; auto]; try apply out_trivial; intro;treat_equalities; apply HNC; assert_diffs; [|ColR..]. assert (Definitions.Col D' B' C); [|ColR]. apply col_conga_col with D' X T; auto. apply col_conga_col with D' B' D'; try apply conga_sym; Col. } assert (HOS2 : OS B' A C D). { apply l9_19 with B; try split; try solve [assert_diffs; ColR]; try (intro; apply HNC; assert_diffs; ColR); repeat split; assert_diffs; Between. } destruct (l11_15 A X T A B' D) as [_ [_ [_ H]]]; try (intro; apply HNC; assert_diffs; ColR). apply H; repeat (split; auto). } assert (HD'' : TS A T B' C). { apply l9_8_2 with B. { split; try (intro; apply HNC; assert_diffs; ColR). split; try (intro; apply HNC; assert_diffs; ColR). exists D; assert_diffs; split; Col. } { apply out_one_side; try (right; intro; apply HNC; assert_diffs; ColR). apply bet2_out_out with X X; try apply out_trivial; assert_diffs; auto. } } destruct HD'' as [_ [_ [D'' [HC' Hb6]]]]. assert (D' = D''); [|subst; auto]. apply l6_21 with B' C A T; Col; intro; apply HNC; assert_diffs; ColR. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype choice seq) mathcomp(fintype finset finfun bigop order) mathcomp(ssralg ssrnum path generic_quotient matrix mxalgebra algC) mathcomp(zmodp) GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.tarski_to_gupta_inspired GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Counter_models.Planar.independence