proposition: Lemma per_lt : forall A B C, A <> B -> C <> B -> Per A B C -> Lt A B A C /\ Lt C B A C.
proof: Proof. intros. assert(Lt B A A C /\ Lt B C A C). apply( l11_46 A B C); auto. spliter. split; apply lt_left_comm; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel