proposition: Lemma pythagoras_obtuse : forall O E E' A B C AC BC AB AC2 BC2 AB2 S2, O<>E -> Obtuse A C B -> Length O E E' A B AB -> Length O E E' A C AC -> Length O E E' B C BC -> Prod O E E' AC AC AC2 -> Prod O E E' BC BC BC2 -> Prod O E E' AB AB AB2 -> Sum O E E' AC2 BC2 S2 -> LtP O E E' S2 AB2.
proof: Proof. intros. unfold Obtuse in H0. ex_and H0 A'. ex_and H8 B'. ex_and H0 C'. assert(A' <> B' /\ C' <> B' /\ C <> A /\ C' <> B' /\ C <> B). { unfold LtA in H8. spliter. unfold LeA in H8. ex_and H8 P. unfold CongA in H10. unfold InAngle in H8. repeat split; try tauto. spliter. auto. spliter. auto. } spliter. assert(HH:=l6_11_existence B' C A A' H9 H11). ex_and HH AA. assert(HH:=l6_11_existence B' C B C' H12 H13). ex_and HH CC. assert(Lt AA CC A B). { apply(t18_18 C A B B' AA CC);Cong. apply lta_comm. apply(lta_out_lta A' B' C' A C B); try(apply l6_6; auto). apply out_trivial; auto. apply out_trivial; auto. auto. } assert(~Col O E E'). { unfold Prod in H5. unfold Ar2 in H5; tauto. } assert(exists S1 : Tpoint, Length O E E' AA CC S1). { apply(length_existence O E E' AA CC);auto. } destruct H20 as [S1 H21]. assert(exists SS : Tpoint, Prod O E E' S1 S1 SS). { apply(prod_exists O E E' H19 S1 S1); unfold Length in H21;tauto. } ex_and H20 SS. apply (per_col _ _ _ CC) in H0;auto. apply l8_2 in H0. apply (per_col _ _ _ AA) in H0;auto. assert(Sum O E E' AC2 BC2 SS). { apply(pythagoras O E E' AA CC B' AC BC S1 AC2 BC2 SS H); auto. apply l8_2; auto. apply(length_eq_cong_2 O E E' A C AA B'); Cong. apply(length_eq_cong_2 O E E' B C CC B'); Cong. } assert(S2=SS). { apply (sum_uniqueness O E E' AC2 BC2);auto. } treat_equalities. assert(HH:= lt_to_ltp O E E' AA CC S1 A B AB H21 H1 H18). assert(Ps O E S1). { assert(AA <> B'). { intro. treat_equalities. unfold Out in H14. contradiction. } assert(CC <> B'). { intro. treat_equalities. unfold Out in H16. contradiction. } assert(AA <> CC). intro. treat_equalities. apply l8_8 in H0. treat_equalities. tauto. apply length_Ps in H21; auto. intro. apply sym_equal in H24. treat_equalities. apply length_cong in H21. treat_equalities. tauto. } apply(square_increase_strict O E E' S1 AB S2 AB2); auto. unfold Length in H1. unfold Length in H21. spliter. repeat split; Col. apply (length_Ps O E E' A B); auto. intro. apply sym_equal in H20. treat_equalities. apply ltP_neg in HH. apply pos_not_neg in H12. contradiction. apply out_col in H14; Col. apply out_col in H16; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order