proposition: Lemma t22_7__obtuse : forall A B C D P Q, Saccheri A B C D -> Bet B P C -> Bet A Q D -> A <> Q -> Per P Q A -> Lt A B P Q -> Obtuse A B C.
proof: Proof. intros A B C D P Q HSac HP HQ HAQ HPerQ Hlt. assert(HSac' := HSac). destruct HSac'. spliter. assert(HPar := sac__pars1423 A B C D HSac). assert(HPar' := sac__pars1234 A B C D HSac). assert(~ Col A B C) by (apply par_strict_not_col_1 with D, HPar'). assert_diffs. assert(B <> P). { intro. subst P. apply HAQ, (l8_7 B); trivial; apply per_col with D; Col. } assert(P <> C). { intro. subst P. assert(D = Q) by (apply (l8_7 C); apply per_col with A; Col; Perp). subst; apply Hlt; Cong. } assert(Q <> D). { intro. subst Q. assert(Col C P D). apply cop_per2__col with A; Perp. apply coplanar_perm_3, col_cop__cop with B; Col; Cop. apply (par_strict_not_col_2 A B C D HPar'); ColR. } assert (LtA B P Q A B C). { apply (conga_preserves_lta B P Q A B P); try (apply conga_refl); auto. apply out2__conga; [apply out_trivial|apply l6_6, bet_out]; auto. apply lt_os_per2__lta; Perp. apply (per_col _ _ D); Col. apply (col_one_side _ D); Col; apply (l9_17 _ _ C); auto. } assert (LtA C P Q A B C). { apply (conga_preserves_lta Q P C P C D); try (apply conga_pseudo_refl); auto. - apply sac__conga in HSac. apply (l11_10 B C D A B C); [CongA|Out..]. - apply lt4321_os_per2__lta. apply (per_col _ _ A); Perp; Col. apply (l8_3 A); Col. apply invert_one_side, (col_one_side _ A); Col; apply one_side_symmetry, (l9_17 _ _ B); Side; Between. apply (cong2_lt__lt A B P Q); Cong. } destruct (angle_partition B P Q) as [HAcute|[HPer|HObtuse]]; auto. - apply lea_obtuse_obtuse with C P Q; [|unfold GeA; Lea]. apply (acute_bet__obtuse B); auto. - exists B, P, Q; auto. - apply lea_obtuse_obtuse with B P Q; [|unfold GeA]; Lea. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma