proposition: Lemma t22_14__sams_nbet : hypothesis_of_acute_saccheri_quadrilaterals -> forall A B C D E F P Q R, ~ Col A B C -> 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.
proof: Proof. intros aah A B C D E F P Q R HNCol HSuma1 HSuma2. assert_diffs. destruct (angle_partition A B C); auto; [destruct (angle_partition A C B); auto|]. - apply (t22_14__sams_nbet_aux A B C); auto. - destruct (l11_43 C A B); auto. 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(HInter := t22_14__sams_nbet_aux C A B G H I P Q R). destruct HInter as [HIsi HNBet]; Col. apply (suma_assoc B C A C A B _ _ _ _ _ _ _ _ _ D E F); SumA. split; auto. apply sams_sym; apply (sams_assoc _ _ _ C A B A B C G H I); SumA. - destruct (l11_43 B A C); auto. assert(HInter := t22_14__sams_nbet_aux B A C D E F P Q R). destruct HInter as [HIsi HNBet]; Col; SumA. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma