proposition: Lemma legendre_aux1 : forall A B C B' C', ~ Col A B C -> Out A B B' -> Out A C C' -> exists D', InAngle D' B A C /\ CongA A C' B' C' B' D' /\ Cong A C' B' D' /\ TS B' C' A D'.
proof: Proof. intros A B C B' C' HNCol HOutB HOutC. assert_diffs. assert (HNCol' : ~ Col A B' C') by (intro; assert_diffs; apply HNCol; ColR). destruct (midpoint_existence B' C') as [M HM]. destruct (symmetric_point_construction A M) as [D' HD]. assert (HNCol1 : ~ Col A M B') by (intro; assert_diffs; apply HNCol'; ColR). assert (HNCol2 : ~ Col D' B' C') by (intro; assert_diffs; apply HNCol'; ColR). exists D'. assert_diffs; destruct HM; destruct HD; split. apply l11_25 with D' B' C'; try (apply out_trivial); auto. repeat split; auto. exists M; split; trivial. right; apply bet_out; auto. destruct (l11_49 A M C' D' M B') as [HCong1 [HConga1 HConga2]]; Cong. apply l11_14; Between. split. apply (l11_10 A C' M M B' D'); Out; CongA. split; Cong. repeat split; Col. exists M; split; Col. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.SPP_ID GeoCoq.Meta_theory.Parallel_postulates.TCP_tarski GeoCoq.Meta_theory.Parallel_postulates.alternate_interior_angles_proclus GeoCoq.Meta_theory.Continuity.angle_archimedes GeoCoq.Meta_theory.Continuity.archimedes GeoCoq.Meta_theory.Continuity.aristotle GeoCoq.Meta_theory.Parallel_postulates.euclid_5_original_euclid GeoCoq.Meta_theory.Parallel_postulates.existential_triangle_rah GeoCoq.Meta_theory.Parallel_postulates.par_perp_perp_TCP GeoCoq.Meta_theory.Parallel_postulates.playfair_alternate_interior_angles GeoCoq.Meta_theory.Parallel_postulates.playfair_bis_playfair GeoCoq.Meta_theory.Parallel_postulates.playfair_universal_posidonius_postulate GeoCoq.Meta_theory.Parallel_postulates.proclus_SPP GeoCoq.Meta_theory.Parallel_postulates.rah_triangle GeoCoq.Meta_theory.Parallel_postulates.tarski_euclid GeoCoq.Meta_theory.Parallel_postulates.triangle_playfair_bis GeoCoq.Meta_theory.Parallel_postulates.triangle_existential_triangle GeoCoq.Meta_theory.Parallel_postulates.universal_posidonius_postulate_par_perp_perp GeoCoq.Tarski_dev.Annexes.defect