proposition: Lemma perp_not_col2 : forall A B C D, Perp A B C D -> ~ Col A B C \/ ~ Col A B D.
proof: Proof. intros. induction (col_dec A B C). right. assert(Perp_at C A B C D). apply l8_14_2_1b_bis; Col. intro. assert(Perp_at D A B C D). apply l8_14_2_1b_bis; Col. assert(C = D). eapply l8_14_3. apply H1. assumption. apply perp_not_eq_2 in H. contradiction. left. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR