proposition: Lemma aristotle__obtuse_case_elimination : aristotle_s_axiom -> ~ hypothesis_of_obtuse_saccheri_quadrilaterals.
proof: Proof. intros aristotle obtuse. destruct ex_lambert as [Q' [C' [P [Q HLam]]]]. assert (HObtuse : Obtuse C' P Q) by (apply <- (lam_obtuse__oah Q'); trivial). assert (HPar : Par_strict Q' Q C' P) by (apply lam__pars1423, HLam). destruct HLam; spliter. destruct (l10_15 P Q P C') as [A' [HPerp HOS]]; Col. apply not_col_permutation_1. apply par_strict_not_col_1 with Q'; Par. assert_diffs. assert (HLtA : LtA Q P A' C' P Q) by (apply obtuse_per__lta; Perp). destruct HLtA as [HLeA HNCongA]. assert (HInAngle : InAngle A' Q P C'). apply lea_in_angle; Side; apply lea_right_comm; trivial. destruct (segment_construction C' P C' P) as [C [HC1 HC2]]. destruct (segment_construction A' P A' P) as [A [HA1 HA2]]. assert_diffs. assert (HInAngle1 : InAngle C A P Q). apply in_angle_reverse with A'; auto. apply l11_24, in_angle_reverse with C'; auto. apply l11_24; trivial. assert (HNCol : ~ Col P C' A'). { intro Habs. apply HNCongA, conga_right_comm, out2__conga. apply out_trivial; auto. apply col_one_side_out with Q; trivial. } assert (HNCol1 : ~ Col P C A) by (intro; apply HNCol; ColR). assert (HNCol2 : ~ Col P Q C) by (intro; apply (par_strict_not_col_2 Q' Q C' P); ColR). assert (HPer : Per A P Q) by (apply l8_2, per_col with A'; Perp; Col). assert (HOS1 : OS A P C Q). apply in_angle_one_side; Col. apply per_not_col; auto. destruct (aristotle P Q A P C) as [X [Y]]; Col. { exists A, P, Q; split; Perp; split. apply inangle__lea; trivial. intro HCongA. assert (Out P C Q) by (apply (conga_os__out A); assumption). apply HNCol2; Col. } spliter. apply (not_and_lt P Q X Y). split; trivial. destruct (l8_18_existence P Q Y) as [Z [HZ1 HZ2]]. intro; assert_diffs; apply HNCol2; ColR. apply lt_transitivity with P Z. - assert (P <> Z). { intro; subst Z. assert_diffs. assert (Per Q P C) by (apply per_col with Y; Col; Perp). apply HNCol1, cop_perp2__col with P Q; Perp; Cop. } assert (HLam : Lambert P X Y Z). { assert_diffs. repeat split; auto. apply per_col with Q; Col. apply l8_2, per_col with A; Perp; Col. apply perp_per_1, perp_left_comm, perp_col with Q; auto. assert (InAngle Y X P Q). apply l11_25 with C A Q; try (apply l6_6); trivial; apply out_trivial; auto. apply coplanar_perm_12, col_cop__cop with Q; Col; Cop. } apply lam_obtuse__lt; trivial. apply <- (lam_obtuse__oah P); trivial. - assert (HOut : Out Q P Z). { apply col_one_side_out with Q'; Col. apply one_side_transitivity with Y. assert_diffs; apply l12_6, par_strict_col_par_strict with C'; Par; ColR. apply l12_6, par_not_col_strict with Y; Col. { apply l12_9 with P Q; Perp; [Cop..| |Cop]. apply coplanar_perm_12, col_cop__cop with C; Col. apply col_cop__cop with C'; Col; Cop. } apply not_col_permutation_1, par_not_col with P C'; Par; ColR. } assert_diffs. apply bet__lt1213; auto. apply out2__bet; trivial. apply col_one_side_out with A; Col. apply one_side_transitivity with Y. { apply l12_6, par_not_col_strict with Y; Col. apply l12_9 with P Q; Perp; [Cop..|]. apply coplanar_perm_12, col_cop__cop with C; Col; Cop. intro; apply HNCol1; ColR. } apply one_side_symmetry, out_out_one_side with C; Side. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.saccheri