proposition: Lemma t22_14__aah : forall A B C D E F P Q R, SumA C A B A B C D E F -> SumA D E F B C A P Q R -> SAMS D E F B C A -> ~ Bet P Q R -> hypothesis_of_acute_saccheri_quadrilaterals.
proof: Proof. intros A B C D E F P Q R HSuma1 HSuma2 HIsi HNBet. destruct(saccheri_s_three_hypotheses) as [|[rah|oah]]; auto; exfalso. - apply HNBet. apply (t22_14__bet rah A B C). apply trisuma_perm_231. exists D, E, F. split; auto. - destruct (col_dec A B C). { apply HNBet. apply (col_trisuma__bet C A B); Col. exists D, E, F. split; auto. } absurd(SAMS D E F B C A); auto. apply t22_14__nsams; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma