proposition: Lemma legendre_aux2 : ~ hypothesis_of_obtuse_saccheri_quadrilaterals -> forall A B C, ~ Col A B C -> Acute B A C -> (forall T, InAngle T B A C -> exists X Y : Tpoint, Out A B X /\ Out A C Y /\ Bet X T Y) -> forall P Q R S T U, Defect A B C P Q R -> GradAExp P Q R S T U -> exists B' C' P' Q' R', (Out A B B' /\ Out A C C' /\ Defect A B' C' P' Q' R' /\ LeA S T U P' Q' R').
proof: Proof. intros noah A B C HNCol HAcute legendre P Q R S T U HDef. induction 1; rename A0 into P; rename B0 into Q; rename C0 into R. exists B; exists C; exists P; exists Q; exists R; assert_diffs. repeat (split; [Out|]); Lea. rename D into S; rename E into T; rename F into U. destruct IHGradAExp as [B' [C' [P' [Q' [R' [HOutB [HOutC [HDef' HLea]]]]]]]]; trivial. destruct (legendre_aux1 A B C B' C') as [D' [HInangle [HConga [HCong HTS]]]]; trivial. assert (HNCol' : ~ Col A B' C') by (destruct HTS; Col). destruct (legendre D' HInangle) as [B'' [C'' [HOutB' [HOutC' HBet]]]]. assert (Hd := defect_distincts A B' C' P' Q' R' HDef'); spliter; assert_diffs. destruct (ex_defect A B'' C'') as [P'' [Q'' [R'' HDef'']]]; auto. intro; subst; apply HNCol; ColR. exists B''; exists C''; exists P''; exists Q''; exists R''. repeat (split; trivial). destruct (ex_suma P' Q' R' P' Q' R') as [V [W [X HSuma1]]]; auto. destruct (legendre_aux noah A B' C' D' B'' C'' P' Q' R' P'' Q'' R'' V W X) as [HIsi1 HLea1]; trivial. apply l6_7 with B; Out. apply l6_7 with C; Out. apply lea_trans with V W X; trivial. apply sams_lea2_suma2__lea with S T U S T U P' Q' R' P' Q' R'; trivial. 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