proposition: Lemma perp_not_eq_3 : forall A B C, Perp A B B C -> A <> C.
proof: Proof. intros. apply perp_comm in H. apply perp_perp_in in H. assert(Per A B C). apply perp_in_per. Perp. unfold Perp_at in H. spliter. intro. subst C. apply l8_8 in H0. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec