proposition: Lemma l8_4 : forall A B C C', Per A B C -> Midpoint B C C' -> Per A B C'.
proof: Proof. unfold Per. intros. ex_and H B'. exists C. split. apply l7_2. assumption. assert (B' = C') by (eapply symmetric_point_uniqueness;eauto). subst B'. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR