proposition: Lemma perp_in_perp_bis : forall A B C D X, Perp_at X A B C D -> Perp X B C D \/ Perp A X C D.
proof: Proof. intros. induction (eq_dec_points X A). subst X. left. unfold Perp. exists A. assumption. right. unfold Perp. exists X. unfold Perp_at in *. spliter. repeat split. intro. apply H0. subst X. reflexivity. assumption. apply col_trivial_3. assumption. intros. apply H4. apply col_permutation_2. eapply col_transitivity_1. intro. apply H0. apply sym_equal. apply H7. Col. Col. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR