proposition: Lemma perp_col4 : forall A B C D P Q R S, P <> Q -> R <> S -> Col A B P -> Col A B Q -> Col C D R -> Col C D S -> Perp A B C D -> Perp P Q R S.
proof: Proof. intros. apply (perp_col2 A B); auto. apply perp_sym, (perp_col2 C D); auto. apply perp_sym, H5. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR