proposition: Lemma t22_24_aux : ~ hypothesis_of_obtuse_saccheri_quadrilaterals -> forall A B0 B00 C0 B C E, ~ Col A B0 C0 -> Perp A C0 B0 C0 -> B0 = B00 -> GradExp2 A B0 B B00 C0 E -> Perp A C0 B C -> Col A C0 C -> Le B0 E B C.
proof: Proof. intros HNob A B0 B00 C0 B C E HNCol HPerp0 Heq HGE. revert C. induction HGE; rename B into B0; rename D into B00; rename E into C0; subst B00. intros C HPerp HCol; assert (C = C0) by (apply (l8_18_uniqueness A C0 B0); Col); subst C; Le. rename C into B; rename C' into B'; rename F into E; rename F' into E'. intros C' HPerp' HCol'. apply gradexp2__gradexp123, gradexp__grad, grad__bet in HGE. destruct (l8_18_existence A C0 B) as [C [HCol HPerp]]. intro; assert_diffs; apply HNCol; ColR. assert (HLe : Le B0 E B C) by (apply IHHGE; trivial). clear IHHGE. destruct (symmetric_point_construction C B) as [D HD]. apply le_transitivity with D C. apply bet2_le2__le1346 with E B; Between; apply (l5_6 B0 E B C); auto with cong. assert (HAC : A <> C). { intro; subst C; assert_diffs; assert (A = C0); auto. apply (l8_18_uniqueness A C0 B0); Col. apply perp_right_comm, perp_col1 with B; Perp; Col. } assert (HAC' : A <> C'). { intro; subst C'; assert_diffs; assert (A = C0); auto. apply (l8_18_uniqueness A C0 B0); Col. apply perp_right_comm, perp_col1 with B'; Perp; ColR. } assert (HPer : Per A C B) by (apply perp_per_1, perp_left_comm, perp_col with C0; assumption). destruct (t22_23 HNob A B' C' B C D) as [_ []]; Perp. - assert_diffs; apply per_not_col in HPer; Col. - apply perp_per_1, perp_col1 with C0; Perp. - split; auto. - ColR. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.saccheri GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Meta_theory.Continuity.grad