proposition: Lemma perp_in_rewrite : forall A B C D P, Perp_at P A B C D -> Perp_at P A P P C \/ Perp_at P A P P D \/ Perp_at P B P P C \/ Perp_at P B P P D.
proof: Proof. intros. assert(HH:= perp_in_col A B C D P H). spliter. induction(eq_dec_points A P); induction(eq_dec_points C P). subst A . subst C. right;right;right. Perp. subst A. right; right; left. apply perp_in_right_comm. assert(HP:=perp_in_col_perp_in P B C D P P H3 H1 H). Perp. subst C. right; left. apply perp_in_sym. apply(perp_in_col_perp_in P D A B P P H2 H0). Perp. left. assert(HP:= perp_in_col_perp_in A B C D P P H3 H1 H). apply perp_in_sym. apply perp_in_left_comm. apply(perp_in_col_perp_in C P A B P P H2 H0). Perp. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel