proposition: Lemma l13_1_aux : forall A B C P Q R, ~ Col A B C -> Midpoint P B C -> Midpoint Q A C -> Midpoint R A B -> exists X, exists Y, Perp_at R X Y A B /\ Perp X Y P Q /\ Coplanar A B C X /\ Coplanar A B C Y.
proof: Proof. intros A B C P Q R HC MBC MAC MAB. assert(Q <> C). intro. subst Q. unfold Midpoint in MAC. spliter. apply cong_identity in H0. subst C. apply HC. Col. assert(P <> C). intro. subst P. unfold Midpoint in MBC. spliter. apply cong_identity in H1. subst C. apply HC. Col. assert(D1:Q<>R). intro. subst R. assert(B=C). apply(symmetric_point_uniqueness A Q); auto. subst C. apply l7_3 in MBC. contradiction. assert(D2:R <> B). intro. subst R. unfold Midpoint in MAB. spliter. apply cong_identity in H2. subst B. apply HC. Col. assert(~Col P Q C). intro. apply HC. unfold Midpoint in *. spliter. apply bet_col in H2. apply bet_col in H4. apply bet_col in H6. ColR. assert(HH:= l8_18_existence P Q C H1). ex_and HH C'. assert(HS1:=symmetric_point_construction C' Q). ex_and HS1 A'. assert(HS1:=symmetric_point_construction C' P). ex_and HS1 B'. assert(Cong C C' B B'). apply(l7_13 P C C' B B' MBC); Midpoint. assert(Cong C C' A A'). apply(l7_13 Q C C' A A'); Midpoint. assert(Per P B' B). induction(eq_dec_points P C'). subst C'. unfold Midpoint in H5. spliter. apply cong_symmetry in H8. apply cong_identity in H8. subst B'. apply l8_2. apply l8_5. apply(symmetry_preserves_per C C' P B B'); Midpoint. apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_left_comm. apply (perp_col _ Q); Col. assert(Per Q A' A). induction(eq_dec_points Q C'). subst C'. unfold Midpoint in H4. spliter. apply cong_symmetry in H9. apply cong_identity in H9. subst A'. apply l8_2. apply l8_5. apply(symmetry_preserves_per C C' Q A A'); Midpoint. apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_left_comm. apply (perp_col _ P); Col. Perp. assert(Cl1: Col A' C' Q). unfold Midpoint in H4. spliter. apply bet_col in H4. Col. assert(Cl2: Col B' C' P). unfold Midpoint in H5. spliter. apply bet_col in H5. Col. assert(NE0: P <> Q). apply perp_distinct in H3; tauto. assert(NE1 : A' <> B'). intro. subst B'. apply NE0. apply (l7_17 C' A'); auto. assert(Cl3: Col A' B' P). induction(eq_dec_points P C'). subst P. unfold Midpoint in H5. spliter. apply cong_symmetry in H10. apply cong_identity in H10. subst C'. Col. induction(eq_dec_points Q C'). subst Q. unfold Midpoint in H4. spliter. apply cong_symmetry in H11. apply cong_identity in H11. subst C'. Col. ColR. assert(Cl4: Col A' B' Q). induction(eq_dec_points P C'). subst P. unfold Midpoint in H5. spliter. apply cong_symmetry in H10. apply cong_identity in H10. subst C'. Col. induction(eq_dec_points Q C'). subst Q. unfold Midpoint in H4. spliter. apply cong_symmetry in H11. apply cong_identity in H11. subst C'. Col. ColR. assert(Cl5:Col A' B' C'). ColR. assert(NE2 : C <> C'). apply perp_distinct in H3. tauto. assert(NE3: A <> A'). intro. subst A'. apply cong_identity in H7. contradiction. assert(NE4: B <> B'). intro. subst B'. apply cong_identity in H6. contradiction. assert(Per P A' A). induction(eq_dec_points A' Q). subst Q. unfold Midpoint in H4. spliter. apply cong_identity in H10. subst C'. clean_trivial_hyps. apply perp_left_comm in H3. apply perp_perp_in in H3. apply perp_in_comm in H3. apply perp_in_per in H3. unfold Midpoint in MAC. spliter. apply bet_col in H2. apply (per_col P A' C A); Col. apply l8_2. apply (per_col A A' Q P); Perp. ColR. assert(Per Q B' B). induction(eq_dec_points B' P). subst P. unfold Midpoint in H5. spliter. apply cong_identity in H11. subst C'. clean_trivial_hyps. apply perp_perp_in in H3. apply perp_in_comm in H3. apply perp_in_per in H3. unfold Midpoint in MBC. spliter. apply bet_col in H2. apply (per_col Q B' C B); Col. apply l8_2. apply (per_col B B' P Q); Perp. ColR. assert(Per A' B' B). apply l8_2. induction(eq_dec_points B' P). subst P. unfold Midpoint in H5. spliter. apply cong_identity in H12. subst C'. clean_trivial_hyps. apply(per_col B B' Q A'); Col; Perp. apply(per_col B B' P A'); Col; Perp. assert(Per B' A' A). apply l8_2. induction(eq_dec_points A' Q). subst Q. unfold Midpoint in H4. spliter. apply cong_identity in H13. subst C'. clean_trivial_hyps. apply(per_col A A' P B'); Col; Perp. apply(per_col A A' Q B'); Col; Perp. assert(NC1 : ~Col A' B' A). apply per_not_col in H13; auto. intro. apply H13. Col. assert(NC2 : ~Col A' B' B). apply per_not_col in H12; auto. assert(HM:=midpoint_existence A' B'). ex_and HM X. assert(HP:=l10_15 A' B' X A). destruct HP as [y []]; Col. assert(HH:=ex_sym X y A). ex_and HH B''. assert( X <> y). apply perp_distinct in H15. spliter. auto. assert(Reflect B'' A X y). unfold Reflect. left. repeat split;auto. ex_and H18 M. exists M. split; Col. assert(Reflect A' B' X y). unfold Reflect. left. split; auto. repeat split. exists X. split; [Midpoint|Col]. left. Perp. apply l10_4 in H20. assert(HH:= l10_10 X y B'' B' A A' H20 H21). assert(Per A' B' B''). unfold Reflect in *. induction H20; induction H21. spliter. apply(image_spec_preserves_per B' A' A A' B' B'' X y); auto. apply l10_4_spec. assumption. spliter. contradiction. spliter. contradiction. spliter. contradiction. unfold Reflect in H21. induction H21. spliter. unfold ReflectL in H23. assert(OS A' B' A B''). induction H17. assert(Par A' B' A B''). assert(Coplanar A y A' X). apply col_cop__cop with B'; Col; Cop. assert(Coplanar A y B' X). apply col_cop__cop with A'; Col; Cop. assert(~ Col A X y). intro. assert(A=B''). apply (image_id X y); Col. assert_diffs. auto. apply(l12_9 A' B' A B'' X y); Perp. Cop. apply coplanar_trans_1 with A; Cop. Cop. apply coplanar_trans_1 with A; Cop. induction H24. apply( l12_6 A' B' A B'' H24). spliter. apply per_not_col in H22; auto. apply False_ind. apply H22. ColR. intro. subst B''. apply cong_symmetry in HH. apply cong_identity in HH. subst A'. apply cong_identity in H7. subst C'. tauto. subst B''. apply one_side_reflexivity. intro. apply NC1. Col. assert(OS A' B' A B). unfold OS. exists C. split. unfold TS. repeat split; Col. intro. apply H1. ColR. exists Q. split; Col. unfold Midpoint in MAC. tauto. unfold TS. repeat split; Col. intro. apply H1. ColR. exists P. split; Col. unfold Midpoint in MBC. tauto. assert( Col B B'' B'). apply cop_per2__col with A'; Perp. apply coplanar_perm_3. apply coplanar_trans_1 with A; Col; Cop. assert(Cong B B' A A'). apply cong_transitivity with C C'; Cong. assert(B = B'' \/ Midpoint B' B B''). apply( l7_20); Col. apply cong_transitivity with A A'; Cong. induction H28. subst B''. exists R. exists X. ex_and H18 M. assert(R = M). apply (l7_17 A B); auto. subst M. assert(A <> B). intro. subst B. apply HC; Col. assert(Col R A B). unfold Midpoint in MAB. spliter. apply bet_col in H31. Col. assert(X <> R). intro. subst X. assert(Par A B A' B'). assert(Coplanar A y A' R). apply col_cop__cop with B'; Col; Cop. assert(Coplanar A y B' R). apply col_cop__cop with A'; Col; Cop. assert(~ Col A R y). intro. assert(A=B). apply (image_id R y); Col. assert_diffs. auto. apply(l12_9 A B A' B' R y); Perp. Cop. Cop. apply coplanar_trans_1 with A; Cop. apply coplanar_trans_1 with A; Cop. induction H17. Perp. contradiction. induction H32. apply H32. exists R. unfold Midpoint in H14. spliter. apply bet_col in H14. split; Col. spliter. apply NC1. Col. split. apply(l8_14_2_1b_bis R X A B R); Col. induction H17. apply perp_left_comm. apply(perp_col _ y); auto. contradiction. split. apply perp_left_comm. apply(perp_col _ y);auto. apply perp_sym. induction(eq_dec_points B' P). subst P. apply(perp_col _ A');auto. Perp. Col. apply(perp_col _ B');auto. apply perp_left_comm. apply(perp_col _ A');auto. Perp. Col. ColR. split. exists R. left. split; Col. assert(Col P Q X). ColR. apply coplanar_pseudo_trans with P Q C; Cop. assert(TS A' B' B B''). unfold TS. repeat split; auto. intro. apply NC2; Col. intro. apply per_not_col in H22; auto. apply H22. Col. intro. subst B''. unfold Midpoint in H28. spliter. apply cong_identity in H30. subst B'. unfold OS in H24. ex_and H24 T. unfold TS in H30. spliter. apply H30. Col. exists B'. split; Col. unfold Midpoint in H28. tauto. assert(OS A' B' B B''). apply (one_side_transitivity A' B' B A ). apply one_side_symmetry. assumption. assumption. apply l9_9 in H29. contradiction. spliter. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel