proposition: Lemma t22_14__bet : hypothesis_of_right_saccheri_quadrilaterals -> forall A B C P Q R, TriSumA A B C P Q R -> Bet P Q R.
proof: Proof. intros rah A B C P Q R HTri. elim(col_dec A B C). intro; apply (col_trisuma__bet A B C); auto. intro. assert_diffs. destruct (angle_partition A B C); auto; [destruct (angle_partition A C B); auto|]. - apply (t22_14__bet_aux A B C); auto. - destruct (l11_43 C A B); auto. apply (t22_14__bet_aux C A B); Col. apply trisuma_perm_312; auto. - destruct (l11_43 B A C); auto. apply (t22_14__bet_aux B A C); Col. apply trisuma_perm_213; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma