proposition: Lemma perp_col2 : forall A B C D X Y, Perp A B X Y -> C <> D -> Col A B C -> Col A B D -> Perp C D X Y.
proof: Proof. intros. assert(HH:=H). apply perp_distinct in HH. spliter. induction (eq_dec_points A C). subst A. apply perp_col with B; Col. assert(Perp A C X Y) by (eapply perp_col;eauto). apply perp_col with A; Perp. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR