proposition: Lemma perp_not_col : forall A B P, Perp A B P A -> ~ Col A B P.
proof: Proof. intros. assert (Perp_at A A B P A). apply perp_perp_in. assumption. assert (Per P A B). apply perp_in_per. apply perp_in_sym. assumption. apply perp_in_left_comm in H0. assert (~ Col B A P -> ~ Col A B P). intro. intro. apply H2. apply col_permutation_4. assumption. apply H2. apply perp_distinct in H. spliter. apply per_not_col. auto. auto. apply perp_in_per. apply perp_in_right_comm. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR