proposition: Lemma t22_12__aah : forall A B C P Q R, Per A B C -> SumA B C A C A B P Q R -> (Acute P Q R <-> hypothesis_of_acute_saccheri_quadrilaterals).
proof: Proof. intros A B C P Q R HPer HSuma. suma.assert_diffs. destruct (per__ex_saccheri B A C) as [D HSac]; auto. assert(HSac' := HSac). unfold Saccheri in HSac'. spliter. assert_diffs. assert(HPars1 := sac__pars1423 B A D C HSac). assert(HPars2 := sac__pars1234 B A D C HSac). assert(TS C A B D) by (apply l9_31; Side). assert(CongA B C D A B C) by CongA. split. - intro. apply (acute_sac__aah B A D C); auto. apply (t22_11__acute _ _ _ C); auto. apply lta_left_comm. apply (sams_lea_lta789_suma2__lta456 B C A _ _ _ P Q R B C A _ _ _ B C D); Lea; SumA. - intro aah. exists B, C, D. split; trivial. apply (sams_lea_lta456_suma2__lta B C A C A B _ _ _ B C A A C D); auto. apply lea_refl; auto. apply lta_left_comm; apply t22_11__acute; try (apply (aah _ _ _ C)); auto. apply os_ts__sams; Side. SumA. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma