proposition: Lemma legendre_aux : greenberg_s_axiom -> triangle_postulate -> forall A B C P Q, Perp Q A P Q -> Perp P B P Q -> Par_strict Q A P B -> Par_strict Q A P C -> OS P B Q C -> OS P Q C A -> OS P Q C B -> False.
proof: Proof. intros greenberg triangle. intros A B C P Q HPerpAP HPerpBP HParAB HParAC HOS1 HOS2 HOS3. destruct (symmetric_point_construction B P) as [B']. assert(HInAngle : InAngle C Q P B) by Side. assert (~ Col P B C) by (apply one_side_not_col124 with Q, HOS1). assert (~ Col P Q C) by (apply one_side_not_col123 with A, HOS2). assert (~ Col P Q A) by (apply one_side_not_col124 with C, HOS2). assert(LtA B P C B P Q). apply inangle__lta; [Col|apply l11_24, HInAngle]. assert(Acute B P C). exists B, P, Q; split; Perp. assert_diffs. destruct (greenberg P Q A B P C) as [R []]; Perp; Col. assert_diffs. assert(OS P Q R A) by (apply invert_one_side, out_one_side; Col). assert(OS P C Q R). apply l12_6, par_strict_col_par_strict with A; Par; Col. destruct (ex_suma B' P R P R Q) as [D [E [F Hsuma1]]]; auto. assert(Htri : TriSumA R Q P D E F). { exists B', P, R; split; auto. apply (conga3_suma__suma B' P Q Q P R B' P R); try (apply conga_refl; auto). - exists R. assert (TS P Q R B'); [|repeat (split; CongA); Side; Cop]. apply (l9_8_2 _ _ B). apply bet__ts; Between; apply one_side_not_col124 with C, HOS3. apply (one_side_transitivity _ _ _ A); [|Side]. apply (one_side_transitivity _ _ _ C); Side. - apply l11_16; auto; apply l8_2. apply per_col with B; Perp; Col. apply per_col with A; Perp; Col. } destruct (ex_suma B' P R C P B) as [I [J [K Hsuma2]]]; auto. assert(~ Col R P B'). { apply (par_not_col Q A); Col. apply par_strict_col_par_strict with B; Col. } assert(Hsuma3 : SumA B' P R R P B B' P B) by (apply bet__suma; Between). assert(Hsams3 : SAMS B' P R R P B) by (apply bet__sams; Between). assert(LeA C P B R P B). { apply lea_comm, inangle__lea, os_ts__inangle. - apply l9_2, (l9_8_2 _ _ Q); trivial. apply invert_two_sides, in_angle_two_sides; Col. - apply (one_side_transitivity _ _ _ Q); trivial. apply one_side_symmetry, l12_6, par_strict_col_par_strict with A; Par; Col. } assert(Habs : LtA D E F B' P B). { apply (lea456789_lta__lta _ _ _ I J K); [|apply (sams_lea2_suma2__lea B' P R C P B _ _ _ B' P R R P B); Lea]. apply (sams_lea_lta456_suma2__lta B' P R P R Q _ _ _ B' P R C P B); Lea. apply (sams_lea2__sams _ _ _ _ _ _ B' P R R P B); Lea. } apply Habs. apply suma_distincts in Hsuma1; spliter. apply conga_line; Between. apply (triangle R Q P); auto. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch13_1