proposition: Lemma t22_12__oah : forall A B C P Q R, Per A B C -> SumA B C A C A B P Q R -> (Obtuse P Q R <-> hypothesis_of_obtuse_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 (obtuse_sac__oah B A D C); auto. apply (t22_11__obtuse _ _ _ C); auto. apply lta_right_comm. apply (sams_lea_lta789_suma2__lta456 B C A _ _ _ B C D B C A _ _ _ P Q R); Lea; [|SumA]. apply os_ts__sams; Side. - intro oah. exists B, C, D. split; trivial. apply (sams_lea_lta456_suma2__lta B C A A C D _ _ _ B C A C A B); SumA. apply lea_refl; auto. apply lta_right_comm; apply t22_11__obtuse; try (apply (oah _ _ _ C)); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma