proposition: Lemma t22_14__nsams : hypothesis_of_obtuse_saccheri_quadrilaterals -> forall A B C D E F, ~ Col A B C -> SumA C A B A B C D E F -> ~ SAMS D E F B C A.
proof: Proof. intros oah A B C D E F HNCol HSuma1. assert_diffs. elim(angle_partition A B C); auto. intro; elim(angle_partition A C B); auto. - intro. apply (t22_14__nsams_aux A B C); auto. - intro. assert(HInter := l11_43 C A B). destruct HInter; Col. assert(HSuma3 := ex_suma B C A C A B). rename H into HAcute. destruct HSuma3 as [G [H [I HSuma3]]]; auto. suma.assert_diffs. assert(HNIsi := t22_14__nsams_aux C A B G H I). intro HIsi. absurd(SAMS G H I A B C). apply HNIsi; Col. apply (sams_assoc B C A C A B _ _ _ _ _ _ D E F); SumA. - intro. assert (HInter := l11_43 B A C). destruct HInter; Col. intro. absurd(SAMS D E F A C B). apply (t22_14__nsams_aux B A C D E F); Col; SumA. SumA. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma