proposition: Lemma not_col_sym_not_col : forall A B B' C , ~Col A B C -> Midpoint A B B' -> ~Col A B' C.
proof: Proof. intros. intro. apply H. unfold Midpoint in H0. spliter. assert(A <> B). intro. subst B. apply H. Col. assert(A <> B'). intro. subst B'. apply cong_identity in H2. subst B. tauto. apply bet_col in H0. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel