proposition: Lemma t22_16_2aux : ~ hypothesis_of_obtuse_saccheri_quadrilaterals -> forall A B C D A1 A2 A3 B1 B2 B3 C1 C2 C3 D1 D2 D3 O P Q R, Defect A B C D1 D2 D3 -> Defect A B D C1 C2 C3 -> Defect A D C B1 B2 B3 -> Defect C B D A1 A2 A3 -> Bet A O C -> Bet B O D -> Col A B C -> SumA D1 D2 D3 B1 B2 B3 P Q R -> SAMS C1 C2 C3 A1 A2 A3 /\ SumA C1 C2 C3 A1 A2 A3 P Q R.
proof: Proof. intros noah A B C D A1 A2 A3 B1 B2 B3 C1 C2 C3 D1 D2 D3 O P Q R HDefD HDefC HDefB HDefA HBet HBet2 HCol HSuma. assert (Hd := defect_distincts A B D C1 C2 C3 HDefC). assert (Hd' := defect_distincts C B D A1 A2 A3 HDefA). assert (Hd'' := defect_distincts A B C D1 D2 D3 HDefD). spliter; suma.assert_diffs. apply col_defect__out in HDefD; trivial. destruct (col_dec A D C) as [HCol1|HNCol]. { assert (Col C B D) by ColR. assert (Col A B D) by ColR. apply col_defect__out in HDefA; trivial. apply col_defect__out in HDefB; trivial. apply col_defect__out in HDefC; trivial. split; [SumA|]. apply (conga3_suma__suma D1 D2 D3 B1 B2 B3 P Q R); try (apply conga_refl); auto; apply l11_21_b; trivial. } assert (B = O) by (apply (l6_21 A C D B); Col). subst O. apply out213_suma__conga in HSuma; trivial. destruct (t22_16_1bis noah A D C B C1 C2 C3 A1 A2 A3 B1 B2 B3) as [HIsi HSuma1]; trivial. apply defect_perm_132, HDefC. apply defect_perm_321, HDefA. split; trivial. apply (conga3_suma__suma C1 C2 C3 A1 A2 A3 B1 B2 B3); CongA. Qed.
imports: GeoCoq.Tarski_dev.Annexes.saccheri