proposition: Lemma per2_preserves_diff : forall O A B A' B', O <> A' -> O <> B' -> Col O A' B' -> Per O A' A -> Per O B' B -> A' <> B' -> A <> B.
proof: Proof. intros. intro. subst B. apply H4. apply(per2_col_eq O A' B' A);Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel