proposition: Lemma l8_20_2 : forall A B C C' D P, Per A B C -> Midpoint P C' D -> Midpoint A C' C -> Midpoint B D C -> B<>C -> A<>P.
proof: Proof. intros. intro. subst P. assert (C = D). eapply symmetric_point_uniqueness. apply H1. assumption. subst D. assert (B = C). apply l7_3. assumption. subst C. absurde. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR