proposition: Lemma greenberg : forall P Q R A B C, ~ Col A B C -> Acute A B C -> Q <> R -> Per P Q R -> exists S, LtA P S Q A B C /\ Out Q S R.
proof: Proof. apply aristotle__greenberg. unfold aristotle_s_axiom; apply aristotle. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.SPP_tarski GeoCoq.Meta_theory.Parallel_postulates.alternate_interior_angles_consecutive_interior_angles GeoCoq.Meta_theory.Parallel_postulates.alternate_interior_angles_playfair_bis GeoCoq.Meta_theory.Parallel_postulates.alternate_interior_angles_triangle GeoCoq.Meta_theory.Parallel_postulates.alternate_interior_angles_proclus GeoCoq.Meta_theory.Parallel_postulates.bachmann_s_lotschnittaxiom_legendre_s_parallel_postulate GeoCoq.Meta_theory.Parallel_postulates.bachmann_s_lotschnittaxiom_weak_inverse_projection_postulate GeoCoq.Meta_theory.Parallel_postulates.bachmann_s_lotschnittaxiom_weak_triangle_circumscription_principle GeoCoq.Meta_theory.Parallel_postulates.consecutive_interior_angles_alternate_interior_angles GeoCoq.Meta_theory.Parallel_postulates.existential_playfair_rah GeoCoq.Meta_theory.Parallel_postulates.existential_saccheri_rah GeoCoq.Meta_theory.Parallel_postulates.inverse_projection_postulate_proclus_bis GeoCoq.Meta_theory.Parallel_postulates.legendre GeoCoq.Meta_theory.Parallel_postulates.midpoint_playfair GeoCoq.Meta_theory.Parallel_postulates.original_euclid_original_spp GeoCoq.Meta_theory.Parallel_postulates.original_spp_inverse_projection_postulate GeoCoq.Meta_theory.Parallel_postulates.par_perp_2_par_par_perp_perp GeoCoq.Meta_theory.Parallel_postulates.par_perp_perp_par_perp_2_par GeoCoq.Meta_theory.Parallel_postulates.par_perp_perp_playfair GeoCoq.Meta_theory.Parallel_postulates.par_trans_playfair GeoCoq.Meta_theory.Parallel_postulates.playfair_existential_playfair GeoCoq.Meta_theory.Parallel_postulates.playfair_midpoint GeoCoq.Meta_theory.Parallel_postulates.playfair_par_trans GeoCoq.Meta_theory.Parallel_postulates.posidonius_postulate_rah GeoCoq.Meta_theory.Parallel_postulates.proclus_aristotle GeoCoq.Meta_theory.Parallel_postulates.proclus_bis_proclus GeoCoq.Meta_theory.Parallel_postulates.rah_existential_saccheri GeoCoq.Meta_theory.Parallel_postulates.rah_rectangle_principle GeoCoq.Meta_theory.Parallel_postulates.rah_similar GeoCoq.Meta_theory.Parallel_postulates.rah_thales_postulate GeoCoq.Meta_theory.Parallel_postulates.rah_posidonius_postulate GeoCoq.Meta_theory.Parallel_postulates.rectangle_existence_rah GeoCoq.Meta_theory.Parallel_postulates.rectangle_principle_rectangle_existence GeoCoq.Meta_theory.Parallel_postulates.similar_rah GeoCoq.Meta_theory.Parallel_postulates.tarski_playfair GeoCoq.Meta_theory.Parallel_postulates.thales_converse_postulate_thales_existence GeoCoq.Meta_theory.Parallel_postulates.thales_converse_postulate_weak_triangle_circumscription_principle GeoCoq.Meta_theory.Parallel_postulates.thales_existence_rah GeoCoq.Meta_theory.Parallel_postulates.thales_postulate_thales_converse_postulate GeoCoq.Meta_theory.Parallel_postulates.weak_inverse_projection_postulate_bachmann_s_lotschnittaxiom GeoCoq.Meta_theory.Parallel_postulates.weak_inverse_projection_postulate_weak_tarski_s_parallel_postulate GeoCoq.Meta_theory.Parallel_postulates.weak_tarski_s_parallel_postulate_weak_inverse_projection_postulate GeoCoq.Meta_theory.Parallel_postulates.weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom GeoCoq.Tarski_dev.Annexes.saccheri GeoCoq.Tarski_dev.Annexes.perp_bisect GeoCoq.Tarski_dev.Annexes.quadrilaterals GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Utils.all_equiv Rtauto