proposition: Lemma t22_16_2aux1 : ~ 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 D -> 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). spliter; suma.assert_diffs. assert (HOut : Out C2 C1 C3) by (apply (col_defect__out A B D); trivial). split; [SumA|]. assert (HSuma1 : SumA C1 C2 C3 A1 A2 A3 A1 A2 A3) by (apply out213__suma; auto). apply (conga3_suma__suma C1 C2 C3 A1 A2 A3 A1 A2 A3); try (apply conga_refl); auto. apply (suma2__conga D1 D2 D3 B1 B2 B3); trivial. destruct (t22_16_2aux noah B A D C B1 B2 B3 A1 A2 A3 D1 D2 D3 C1 C2 C3 O A1 A2 A3); Col; apply defect_perm_213; trivial. Qed.
imports: GeoCoq.Tarski_dev.Annexes.saccheri