proposition: Lemma col_per2_cases : forall A B C D B', B <> C -> B' <> C -> C <> D -> Col B C D -> Per A B C -> Per A B' C -> B = B' \/ ~Col B' C D.
proof: Proof. intros. induction(eq_dec_points B B'). left; auto. right. intro. assert(Col C B B'). ColR. assert(Per A B' B). apply(per_col A B' C B H0 H4); Col. assert(Per A B B'). apply(per_col A B C B' H H3); Col. apply H5. apply (l8_7 A); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR