proposition: Lemma t22_7__acute : 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 P Q A B -> Acute 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(P <> Q) by (intro; apply HPar; exists P; subst; split; Col). 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(Hlta1 : LtA A B C B P Q). { apply (conga_preserves_lta A B P B P Q); try (apply conga_refl); auto. apply out2__conga; Out. apply lt4321_os_per2__lta; Le; Perp. apply (per_col _ _ D); Col. apply (col_one_side _ D); Col; apply (l9_17 _ _ C); auto. } assert(Hlta2 : LtA A B C C P Q). { apply (conga_preserves_lta D C P C P Q); try (apply conga_refl); auto. - apply sac__conga in HSac. apply (l11_10 D C B A B C); [CongA|Out..]. - apply lt4321_os_per2__lta; auto. apply (per_col _ _ A); Perp; Col. apply (l8_3 A); Perp; Col. apply (col_one_side _ A); Col; apply (l9_17 _ _ B); Between; Side. apply (cong2_lt__lt P Q A B); Cong. } destruct (angle_partition B P Q) as [HAcute|[HPer|HObtuse]]; auto. - apply acute_lea_acute with B P Q; Lea. - exists B, P, Q; auto. - apply acute_lea_acute with C P Q; Lea. apply (bet_obtuse__acute B); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma