proposition: Lemma t22_14__oah : forall A B C D E F, SumA C A B A B C D E F -> ~ SAMS D E F B C A -> hypothesis_of_obtuse_saccheri_quadrilaterals.
proof: Proof. intros A B C D E F HSuma1 HNIsi. suma.assert_diffs. destruct(col_dec A B C). { exfalso. apply HNIsi. destruct(bet_dec A B C). - apply out546__sams; Out. - apply (conga2_sams__sams C A B B C A); try (apply conga_refl); SumA. apply (out546_suma__conga _ _ _ A B C); auto. apply not_bet_out; auto. } assert(HSuma2 := ex_suma D E F B C A). destruct HSuma2 as [P [Q [R HSuma2]]]; auto. destruct (saccheri_s_three_hypotheses) as [aah|[rah|]]; auto; exfalso; apply HNIsi. - apply t22_14__sams_nbet with P Q R; assumption. - apply bet_suma__sams with P Q R; trivial. apply (t22_14__bet rah C A B). exists D, E, F; split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma