proposition: Lemma t22_12__rah : forall A B C, A <> B -> B <> C -> Per A B C -> (SumA B C A C A B A B C <-> hypothesis_of_right_saccheri_quadrilaterals).
proof: Proof. intros A B C HAB HBC HPer. destruct (per__ex_saccheri B A C) as [D HSac]; auto. 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_diffs. assert(CongA B C D A B C) by (unfold Saccheri in HSac; spliter; CongA). split. - intro. apply (per_sac__rah B A D C); auto. apply (t22_11__per _ _ _ C); auto. apply conga_left_comm. apply (sams2_suma2__conga456 B C A _ _ _ _ _ _ A B C); try (apply sams123231); auto. apply os_ts__sams; Side. exists D. repeat (split; CongA); Side; Cop. - intro rah. apply (conga3_suma__suma B C A A C D B C D); try (apply conga_refl); auto. exists D; repeat (split; CongA); Side; Cop. apply conga_sym. apply conga_left_comm. apply t22_11__per; auto. apply (rah _ _ _ C); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma