proposition: Lemma per_not_colp : forall A B P R, A <> B -> A <> P -> B <> R -> Per B A P -> Per A B R -> ~Col P A R.
proof: Proof. intros. intro. assert (Perp A B P A). apply perp_comm. apply per_perp; auto. assert (Perp A B B R). apply per_perp; auto. assert (Per B A R). eapply per_col. apply H0. assumption. ColR. apply l8_2 in H3. apply l8_2 in H7. assert (A = B). eapply l8_7. apply H7. assumption. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR