proposition: Lemma per_diff : forall A B A' B' P, A <> B -> ~ Col A B A' -> Per A A' P -> Per B B' P -> A' <> P -> B' <> P -> A' <> B'.
proof: Proof. intros. intro. subst B'. apply H0. eapply per2__col. apply H1. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec