proposition: Lemma per2_col_eq : forall A P P' B, A <> P -> A <> P' -> Per A P B -> Per A P' B -> Col P A P' -> P = P'.
proof: Proof. intros. induction(eq_dec_points P B). subst B. assert( A = P' \/ P = P'). apply(l8_9 A P' P H2); Col. induction H4. contradiction. assumption. induction(eq_dec_points P' B). subst B. assert(A = P \/ P' = P). apply(l8_9 A P P' H1); Col. induction H5; auto. contradiction. apply per_perp_in in H1; auto. apply per_perp_in in H2; auto. apply perp_in_comm in H1. apply perp_in_comm in H2. apply perp_in_perp_bis in H1. apply perp_in_perp_bis in H2. induction H1; induction H2. apply(l8_18_uniqueness P A B P P'); Col. apply perp_not_col; auto. apply perp_left_comm. apply(perp_col A P' B P' P); Perp. Col. apply perp_distinct in H2. tauto. apply perp_distinct in H1. tauto. apply perp_distinct in H1. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel