proposition: Lemma t22_16_1bis : ~ hypothesis_of_obtuse_saccheri_quadrilaterals -> forall A B C C1 D E F G H I K L M, Bet A C1 C -> Defect A B C1 D E F -> Defect B C1 C G H I -> Defect A B C K L M -> SAMS D E F G H I /\ SumA D E F G H I K L M.
proof: Proof. intros noah A B C C1 D E F G H I K L M HBet HDefA HDefB HDef. assert (Hd := defect_distincts A B C1 D E F HDefA). assert (Hd' := defect_distincts B C1 C G H I HDefB). spliter. destruct (ex_suma D E F G H I) as [K' [L' [M' HSuma]]]; auto. destruct (t22_16_1 noah A B C C1 D E F G H I K' L' M') as [HIsi HDef']; trivial. split; trivial. apply (conga3_suma__suma D E F G H I K' L' M'); try (apply conga_refl); auto. apply (defect2__conga A B C); trivial. Qed.
imports: GeoCoq.Tarski_dev.Annexes.saccheri