proposition: Lemma PythOK : forall O E E' A B C A2 B2 C2, PythRel O E E' A B C -> Prod O E E' A A A2 -> Prod O E E' B B B2 -> Prod O E E' C C C2 -> Sum O E E' A2 B2 C2.
proof: Proof. intros. unfold PythRel in H. spliter. unfold Ar2 in H. spliter. induction H3. spliter. subst B. assert(B2=O). apply (prod_O_l_eq O E E' O); auto. subst B2. assert(A2 = C2). induction H7. subst C. apply (prod_uniqueness O E E' A A); auto. assert(Prod O E E' C C A2). apply(opp_same_square O E E' A); auto. apply (prod_uniqueness O E E' C C); auto. subst C2. apply (sum_A_O O E E' ); auto. unfold Prod in H0. spliter. unfold Ar2 in H0; tauto. assert(O <> E). intro. subst E. apply H. Col. ex_and H3 B'. assert(Per A O B'). apply l8_2. apply (per_col _ _ B). apply perp_distinct in H3. tauto. apply perp_in_per. apply perp_in_comm. apply perp_perp_in. Perp. ColR. induction(eq_dec_points A O). subst A. assert(Cong O B O C). apply cong_transitivity with O B'; Cong. assert(B = C \/ Midpoint O B C). apply l7_20; auto. ColR. induction H12. subst C. assert(B2 = C2). apply(prod_uniqueness O E E' B B); auto. subst C2. assert(A2=O). apply(prod_uniqueness O E E' O O); auto. apply prod_0_l; auto. subst A2. apply sum_O_B; Col. unfold Prod in H2. spliter. unfold Ar2 in H2. tauto. assert(A2=O). apply(prod_uniqueness O E E' O O); auto. apply prod_0_l; auto. subst A2. apply (midpoint_opp O E E') in H12; unfold Midpoint in H12. assert(C2 = B2). apply(prod_uniqueness O E E' C C);auto. apply (opp_same_square O E E' B C); auto. subst C2. apply sum_O_B; auto. unfold Prod in H2. spliter. unfold Ar2 in H2. tauto. unfold Ar2. repeat split; auto. induction(out_dec O A E); induction(out_dec O B E);induction(out_dec O C E). apply(pythagoras O E E' A B' O A B C A2 B2 C2); auto. unfold Length. repeat split; auto. unfold LeP. left. unfold LtP. exists C. split. apply sum_diff. apply sum_O_B; Col. unfold Ps. assumption. unfold Length. repeat split; Cong. unfold LeP. left. unfold LtP. exists A. split. apply sum_diff. apply sum_O_B; Col. unfold Ps. assumption. unfold Length. repeat split; Cong. unfold LeP. left. unfold LtP. exists B. split. apply sum_diff. apply sum_O_B; Col. unfold Ps. assumption. assert(exists OC : Tpoint, Opp O E E' C OC). apply(opp_exists O E E' H C). Col. ex_and H15 OC. assert(Ng O E C). unfold Ng. repeat split; auto. intro. subst C. apply cong_symmetry in H9. apply cong_identity in H9. subst B'. apply perp_right_comm in H3. apply perp_not_col in H3. apply H3. ColR. apply not_out_bet in H14. assumption. Col. assert(Ps O E OC). apply(opp_neg_pos O E E' C OC); auto. apply(pythagoras O E E' A B' O A B OC A2 B2 C2); auto. unfold Length. repeat split; auto. unfold Ps in H16. apply out_col in H17. Col. unfold LeP. left. unfold LtP. exists OC. split; auto. apply diff_A_O; auto. unfold Ps in H17. Col. apply opp_midpoint in H16. unfold Midpoint in H16. spliter. apply cong_transitivity with O C; Cong. unfold Length. repeat split; Cong. unfold LeP. left. unfold LtP. exists A. split. apply sum_diff. apply sum_O_B; Col. unfold Ps. assumption. unfold Length. repeat split; Cong. unfold LeP. left. unfold LtP. exists B. split. apply sum_diff. apply sum_O_B; Col. unfold Ps. assumption. apply(opp_same_square O E E' C OC C2 H16 H2). assert(exists OB : Tpoint, Opp O E E' B OB). apply(opp_exists O E E' H B). Col. ex_and H15 OB. assert(Ng O E B). unfold Ng. repeat split; auto. intro. subst B. apply cong_identity in H8. subst B'. apply perp_distinct in H3. tauto. apply not_out_bet in H13. assumption. Col. assert(Ps O E OB). apply(opp_neg_pos O E E' B OB); auto. apply(pythagoras O E E' A B' O A OB C A2 B2 C2); auto. unfold Length. repeat split; auto. unfold Ps in H17. apply out_col in H17. Col. unfold LeP. left. unfold LtP. exists C. split; auto. apply diff_A_O; auto. unfold Ps in H17. Col. unfold Length. repeat split; Cong. unfold LeP. left. unfold LtP. exists A. split. apply sum_diff. apply sum_O_B; Col. unfold Ps. assumption. unfold Length. repeat split; Cong; Col. unfold LeP. left. unfold LtP. exists OB. split; auto. apply diff_A_O; auto. Col. apply opp_midpoint in H16. unfold Midpoint in H16. spliter. apply cong_transitivity with O B; Cong. apply(opp_same_square O E E' B OB B2 H16 H1). assert(exists OC : Tpoint, Opp O E E' C OC). apply(opp_exists O E E' H C). Col. ex_and H15 OC. assert(Ng O E C). unfold Ng. repeat split; auto. intro. subst C. apply cong_symmetry in H9. apply cong_identity in H9. subst B'. apply perp_right_comm in H3. apply perp_not_col in H3. apply H3. ColR. apply not_out_bet in H14. assumption. Col. assert(Ps O E OC). apply(opp_neg_pos O E E' C OC); auto. assert(exists OB : Tpoint, Opp O E E' B OB). apply(opp_exists O E E' H B). Col. ex_and H18 OB. assert(Ng O E B). unfold Ng. repeat split; auto. intro. subst B. apply cong_identity in H8. subst B'. apply perp_distinct in H3. tauto. apply not_out_bet in H13. assumption. Col. assert(Ps O E OB). apply(opp_neg_pos O E E' B OB); auto. apply(pythagoras O E E' A B' O A OB OC A2 B2 C2); auto. unfold Length. repeat split; auto. unfold Ps in H17. apply out_col in H17. Col. unfold LeP. left. unfold LtP. exists OC. split; auto. apply diff_A_O; auto. unfold Ps in H17. Col. apply opp_midpoint in H16. unfold Midpoint in H16. spliter. apply cong_transitivity with O C; Cong. unfold Length. repeat split; Cong. unfold LeP. left. unfold LtP. exists A. split. apply sum_diff. apply sum_O_B; Col. unfold Ps. assumption. unfold Length. repeat split; Cong; Col. unfold LeP. left. unfold LtP. exists OB. split; auto. apply diff_A_O; auto. Col. apply opp_midpoint in H19. unfold Midpoint in H19. spliter. apply cong_transitivity with O B; Cong. apply(opp_same_square O E E' B OB B2 H19 H1). apply(opp_same_square O E E' C OC C2 H16 H2). assert(exists OA : Tpoint, Opp O E E' A OA). apply(opp_exists O E E' H A). Col. ex_and H15 OA. assert(Ng O E A). unfold Ng. repeat split; auto. apply not_out_bet in H12;auto. Col. apply(pythagoras O E E' A B' O OA B C A2 B2 C2); auto. unfold Length. repeat split; auto. unfold LeP. left. unfold LtP. exists C. split. apply sum_diff. apply sum_O_B; Col. unfold Ps. assumption. assert(Col O E OA). unfold Opp in H16. unfold Sum in H16. spliter. unfold Ar2 in H16. tauto. unfold Length. repeat split; auto. unfold LeP. left. unfold LtP. exists OA. split. apply sum_diff. apply sum_O_B; Col. unfold Ps. apply opp_midpoint in H16. unfold Midpoint in H16. spliter. apply not_out_bet in H12. assert(HP:=l5_2 A O E OA H11 H12 H16). unfold Out. repeat split; auto. intro. subst OA. apply cong_identity in H18. contradiction. induction HP. right; auto. left; auto. Col. unfold Opp in H16. apply opp_midpoint in H16. unfold Midpoint in H16. unfold Sum in H16. spliter. Cong. unfold Length. repeat split; Cong. unfold LeP. left. unfold LtP. exists B. split. apply sum_diff. apply sum_O_B; Col. unfold Ps. assumption. apply(opp_same_square O E E' A OA A2 H16 H0). assert(exists OC : Tpoint, Opp O E E' C OC). apply(opp_exists O E E' H C). Col. ex_and H15 OC. assert(Ng O E C). unfold Ng. repeat split; auto. intro. subst C. apply cong_symmetry in H9. apply cong_identity in H9. subst B'. apply perp_right_comm in H3. apply perp_not_col in H3. apply H3. ColR. apply not_out_bet in H14. assumption. Col. assert(Ps O E OC). apply(opp_neg_pos O E E' C OC); auto. assert(exists OA : Tpoint, Opp O E E' A OA). apply(opp_exists O E E' H A). Col. ex_and H18 OA. assert(Ng O E A). unfold Ng. repeat split; auto. apply not_out_bet in H12;auto. Col. assert(Col O E OA). unfold Opp in H19. unfold Sum in H19. spliter. unfold Ar2 in H19. tauto. apply(pythagoras O E E' A B' O OA B OC A2 B2 C2); auto. unfold Length. repeat split; auto. unfold Ps in H17. apply out_col in H17. Col. unfold LeP. left. unfold LtP. exists OC. split; auto. apply diff_A_O; auto. unfold Ps in H17. Col. apply opp_midpoint in H16. unfold Midpoint in H16. spliter. apply cong_transitivity with O C; Cong. unfold Length. repeat split; auto. unfold LeP. left. unfold LtP. exists OA. split. apply sum_diff. apply sum_O_B; Col. unfold Ps. apply opp_midpoint in H19. unfold Midpoint in H19. spliter. apply not_out_bet in H12. assert(HP:=l5_2 A O E OA H11 H12 H19). unfold Out. repeat split; auto. intro. subst OA. apply cong_identity in H21. contradiction. induction HP. right; auto. left; auto. Col. apply opp_midpoint in H19. unfold Midpoint in H19. spliter. Cong. unfold Length. repeat split; Cong. unfold LeP. left. unfold LtP. exists B. split. apply sum_diff. apply sum_O_B; Col. unfold Ps. assumption. apply(opp_same_square O E E' A OA A2 H19 H0). apply(opp_same_square O E E' C OC C2 H16 H2). assert(exists OB : Tpoint, Opp O E E' B OB). apply(opp_exists O E E' H B). Col. ex_and H15 OB. assert(Ng O E B). unfold Ng. repeat split; auto. intro. subst B. apply cong_identity in H8. subst B'. apply perp_distinct in H3. tauto. apply not_out_bet in H13. assumption. Col. assert(Ps O E OB). apply(opp_neg_pos O E E' B OB); auto. assert(exists OA : Tpoint, Opp O E E' A OA). apply(opp_exists O E E' H A). Col. ex_and H18 OA. assert(Ng O E A). unfold Ng. repeat split; auto. apply not_out_bet in H12;auto. Col. assert(Col O E OA). unfold Opp in H19. unfold Sum in H19. spliter. unfold Ar2 in H19. tauto. apply(pythagoras O E E' A B' O OA OB C A2 B2 C2); auto. unfold Length. repeat split; auto. unfold LeP. left. unfold LtP. exists C. split. apply sum_diff. apply sum_O_B; Col. auto. unfold Length. repeat split; auto. unfold LeP. left. unfold LtP. exists OA. split. apply sum_diff. apply sum_O_B; Col. unfold Ps. apply opp_midpoint in H19. unfold Midpoint in H19. spliter. apply not_out_bet in H12. assert(HP:=l5_2 A O E OA H11 H12 H19). unfold Out. repeat split; auto. intro. subst OA. apply cong_identity in H21. contradiction. induction HP. right; auto. left; auto. Col. apply opp_midpoint in H19. unfold Midpoint in H19. spliter. Cong. unfold Length. repeat split; Cong; Col. unfold LeP. left. unfold LtP. exists OB. split; auto. apply diff_A_O; auto. Col. apply opp_midpoint in H16. unfold Midpoint in H16. spliter. apply cong_transitivity with O B; Cong. apply(opp_same_square O E E' A OA A2 H19 H0). apply(opp_same_square O E E' B OB B2 H16 H1). assert(exists OC : Tpoint, Opp O E E' C OC). apply(opp_exists O E E' H C). Col. ex_and H15 OC. assert(Ng O E C). unfold Ng. repeat split; auto. intro. subst C. apply cong_symmetry in H9. apply cong_identity in H9. subst B'. apply perp_right_comm in H3. apply perp_not_col in H3. apply H3. ColR. apply not_out_bet in H14. assumption. Col. assert(Ps O E OC). apply(opp_neg_pos O E E' C OC); auto. assert(exists OA : Tpoint, Opp O E E' A OA). apply(opp_exists O E E' H A). Col. ex_and H18 OA. assert(Ng O E A). unfold Ng. repeat split; auto. apply not_out_bet in H12;auto. Col. assert(Col O E OA). unfold Opp in H19. unfold Sum in H19. spliter. unfold Ar2 in H19. tauto. assert(exists OB : Tpoint, Opp O E E' B OB). apply(opp_exists O E E' H B). Col. ex_and H21 OB. assert(Ng O E B). unfold Ng. repeat split; auto. intro. subst B. apply cong_identity in H8. subst B'. apply perp_distinct in H3. tauto. apply not_out_bet in H13. assumption. Col. assert(Ps O E OB). apply(opp_neg_pos O E E' B OB); auto. apply(pythagoras O E E' A B' O OA OB OC A2 B2 C2); auto. unfold Length. repeat split; auto. unfold Ps in H17. apply out_col in H17. Col. unfold LeP. left. unfold LtP. exists OC. split; auto. apply diff_A_O; auto. unfold Ps in H17. Col. apply opp_midpoint in H16. unfold Midpoint in H16. spliter. apply cong_transitivity with O C; Cong. unfold Length. repeat split; auto. unfold LeP. left. unfold LtP. exists OA. split. apply sum_diff. apply sum_O_B; Col. unfold Ps. apply opp_midpoint in H19. unfold Midpoint in H19. spliter. apply not_out_bet in H12. assert(HP:=l5_2 A O E OA H11 H12 H19). unfold Out. repeat split; auto. intro. subst OA. apply cong_identity in H24. contradiction. induction HP. right; auto. left; auto. Col. apply opp_midpoint in H19. unfold Midpoint in H19. spliter. Cong. unfold Length. repeat split; Cong; Col. unfold LeP. left. unfold LtP. exists OB. split; auto. apply diff_A_O; auto. Col. apply opp_midpoint in H22. unfold Midpoint in H22. spliter. apply cong_transitivity with O B; Cong. apply(opp_same_square O E E' A OA A2 H19 H0). apply(opp_same_square O E E' B OB B2 H22 H1). apply(opp_same_square O E E' C OC C2 H16 H2). Qed.
imports: GeoCoq.Tarski_dev.Ch16_coordinates