proposition: Lemma t22_14__rah : forall A B C P Q R, ~ Col A B C -> TriSumA A B C P Q R -> Bet P Q R -> hypothesis_of_right_saccheri_quadrilaterals.
proof: Proof. intros A B C P Q R HNCol HTri HBet. apply trisuma_perm_312 in HTri. destruct (saccheri_s_three_hypotheses) as [aah|[|oah]]; auto; exfalso. - destruct HTri as [D [E [F []]]]. assert(HInter := t22_14__sams_nbet aah A B C D E F P Q R). destruct HInter; auto. - exfalso. destruct HTri as [D [E [F [HSuma1 HSuma2]]]]. apply (t22_14__nsams oah A B C D E F); auto. destruct HSuma2 as [G [HConga1 [HNos [HCop HConga2]]]]. apply conga_sym in HConga1. assert_diffs. apply (sams_chara _ _ _ _ _ _ G); Lea. apply (bet_conga__bet P Q R); CongA. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma