proposition: Lemma t22_20 : ~ hypothesis_of_obtuse_saccheri_quadrilaterals -> forall A B C D E F, SumA A B C B C A D E F -> SAMS D E F C A B.
proof: Proof. intros noah A B C D E F HS. destruct(sams_dec D E F C A B); trivial. exfalso. apply noah, (t22_14__oah B C A D E F); trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma