proposition: Lemma t22_23 : ~ hypothesis_of_obtuse_saccheri_quadrilaterals -> forall A B C M N L, ~ Col A M N -> Per B C A -> A <> C -> Midpoint M A B -> Per M N A -> Col A C N -> Midpoint M N L -> Bet A N C /\ Le N C A N /\ Le L N B C.
proof: Proof. intros HNob A B C M N L HNCol HPerC HAC HM HPerN HColN HN. destruct (t22_23_aux A B C M N L) as [HBet [HLam HCong]]; auto. split; auto. assert (HLBC : ~ Obtuse L B C) by (intro; apply HNob, (lam_obtuse__oah N L B C); trivial). assert (Hos1 : OS N L B C) by (apply lam__os; trivial). assert (Hos2 : OS N C B L) by (apply lam__os, lam_perm; trivial). unfold Lambert in HLam; spliter. destruct (angle_partition L B C) as [HAcute | [HPer | HObtuse]]; trivial; [ | | exfalso; auto]. - split; apply lt__le; [apply (cong2_lt__lt N C B L); Cong | ]. apply lta_os_per2__lt; Perp; Side; apply lta_left_comm, acute_per__lta; auto. apply lt_left_comm, lta_os_per2__lt; Side; apply acute_per__lta; auto. - split; apply cong__le; [apply cong_transitivity with B L; trivial | apply cong_left_commutativity]; apply conga_per2_os__cong; Perp; Side; apply l11_16; Perp. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.saccheri GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Meta_theory.Continuity.grad