proposition: Lemma l8_3 : forall A B C A', Per A B C -> A<>B -> Col B A A' -> Per A' B C.
proof: Proof. unfold Per. intros. ex_and H C'. exists C'. split. assumption. unfold Midpoint in *;spliter. apply l4_17 with A B; Col; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR