proposition: Lemma pythagoras_acute : forall O E E' A B C AC BC AB AC2 BC2 AB2 S2, O<>E -> Acute 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' AB2 S2.
proof: Proof. intros. unfold Acute in H0. ex_and H0 A'. ex_and H8 B'. ex_and H0 C'. assert(A <> C /\ B <> C). { split; intro; treat_equalities; unfold LtA in H8; spliter; unfold LeA in H8; ex_and H8 P; unfold CongA in *; tauto. } spliter. assert(~Col O E E'). { unfold Prod in H5. unfold Ar2 in H5; tauto. } induction(eq_dec_points A B). { treat_equalities. assert(Length O E E' A A O). { apply length_id_2; auto. } assert(AB = O). { apply (length_uniqueness O E E' A A); auto. } apply sym_equal in H12. treat_equalities. apply(prod_O_l_eq) in H6. subst AB2. apply length_Ps in H2. apply length_Ps in H3. assert(Ps O E AC2). { apply (signeq__prod_pos O E E' AC AC); auto. unfold SignEq. left. split; auto. } assert(Ps O E BC2). { apply (signeq__prod_pos O E E' BC BC); auto. unfold SignEq. left. split; auto. } apply sum_pos_pos in H7; auto. unfold LtP. exists S2. split; auto. apply(diff_A_O O E E' S2 ); auto. unfold Ps in H2. apply out_col in H2; Col. intro. subst BC. apply length_cong in H3. treat_equalities; tauto; apply sym_equal in H6. intro. subst AC. apply length_cong in H2. treat_equalities; tauto. } { assert(A' <> B' /\ 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; tauto. } spliter. assert(exists X : Tpoint, Out B' X A' /\ Cong B' X C A). { apply(l6_11_existence B' C A A' H13); auto. } ex_and H16 AA. assert(exists X : Tpoint, Out B' X C' /\ Cong B' X C B). { apply(l6_11_existence B' C B C'); auto. } ex_and H18 CC. assert(Lt A B AA CC). { apply(t18_18 B' AA CC C A B );Cong. apply lta_comm. apply(lta_out_lta A C B A' B' C'); try(apply l6_6; auto). apply out_trivial; auto. apply out_trivial; auto. auto. } assert(exists S1 : Tpoint, Length O E E' AA CC S1). { apply(length_existence O E E' AA CC);auto. } destruct H21 as [S1 H22]. assert(exists SS : Tpoint, Prod O E E' S1 S1 SS). { apply(prod_exists O E E' H11 S1 S1); unfold Length in H22;tauto. } ex_and H21 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' A B AB AA CC S1 H1 H22 H20). apply(square_increase_strict O E E' AB S1 AB2 S2); auto. unfold Length in H1. unfold Length in H22. spliter. repeat split; Col. apply (length_Ps O E E' A B) in H1. auto. intro. apply sym_equal in H15. treat_equalities. apply (length_cong O E E') in H1. treat_equalities. tauto. 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 H22; auto. intro. apply sym_equal in H25. treat_equalities. apply length_cong in H22. treat_equalities. tauto. apply out_col in H16; Col. apply out_col in H18; Col. } Qed.
imports: GeoCoq.Tarski_dev.Ch14_order