proposition: Lemma per_id : forall A B B' C, A <> B -> B <> C -> B' <> C -> Per A B C -> Per A B' C -> Col C B B' -> B = B'.
proof: Proof. intros. assert(~ Col A B C). eapply per_not_col. assumption. assumption; assert(Per B B' C). eapply (l8_3 A); try auto. Col. assert(A <> B'). intro. subst B'. apply H5. Col. assert(Per A B B'). eapply (per_col _ _ C); auto. Col. assert(Per A B' B). eapply (per_col _ _ C); auto. Col. eapply l8_7. apply H7. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec