proposition: Lemma perp_col1 : forall A B C D X, C <> X -> Perp A B C D -> Col C D X -> Perp A B C X.
proof: Proof. intros. assert (T:=perp_distinct A B C D H0). spliter. unfold Perp in *. ex_and H0 P. exists P. unfold Perp_at in *. spliter. repeat split. assumption. assumption. assumption. apply col_permutation_2. eapply col_transitivity_2. intro. apply H3. apply sym_equal. apply H8. apply col_permutation_4. assumption. apply col_permutation_3. assumption. intros. apply H7. assumption. apply col_permutation_2. eapply col_transitivity_1. apply H. apply col_permutation_5. assumption. apply col_permutation_1. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR