proposition: Lemma legendre_aux2 : greenberg_s_axiom -> triangle_postulate -> forall A1 A2 B1 B2 C1 C2 P, Perp2 A1 A2 B1 B2 P -> ~ Col A1 A2 P -> Col P B1 B2 -> Coplanar A1 A2 B1 B2 -> Par A1 A2 C1 C2 -> Col P C1 C2 -> Col C1 B1 B2.
proof: Proof. intros greenberg triangle. intros A1 A2 B1 B2 C1 C2 P HPerp2 HNC HPB HCop HParAC HPC. assert(HParAB : Par_strict A1 A2 B1 B2) by (apply (col_cop_perp2__pars_bis P); Col). apply (legendre_aux1 greenberg triangle A1 A2 _ _ _ C2 P); auto. intro Hts. assert(HC1NotB : ~ Col C1 B1 B2) by (destruct Hts as [_ []]; auto). assert(C1<>P) by (intro; subst C1; Col). destruct (symmetric_point_construction C1 P) as [C3]. assert_diffs. assert(HC3NotB : ~ Col C3 B1 B2) by (intro; apply HC1NotB; ColR). apply HC3NotB. apply (legendre_aux1 greenberg triangle A1 A2 _ _ _ C1 P); Col. - apply par_right_comm. apply (par_col_par _ _ _ P); Col. apply (par_col_par _ _ _ C2); Col. - apply l9_9_bis. exists C1. repeat (split; [assumption|]). exists P. split; Between. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch13_1