proposition: Lemma perp_col0 : forall A B C D X Y, Perp A B C D -> X <> Y -> Col A B X -> Col A B Y -> Perp C D X Y.
proof: Proof. unfold Perp. intros. ex_and H X0. exists X0. unfold Perp_at in *. spliter. repeat split. assumption. assumption. assumption. eapply col3. apply H. Col. assumption. assumption. intros. apply l8_2. apply H6. assert(Col A X Y). eapply col3 with A B;Col. assert (Col B X Y). eapply col3 with A B;Col. eapply col3 with X Y;Col. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR