proposition: Lemma not_col_par_col_diff : forall A B C D E, ~ Col A B C -> Par A B C D -> Col C D E -> A <> E.
proof: Proof. intros A B C D E HNC HPar HC. intro; subst. apply HNC; apply not_strict_par1 with D E; finish. Qed.
imports: GeoCoq.Highschool.circumcenter