proposition: Lemma perp_in_sym : forall A B C D X, Perp_at X A B C D -> Perp_at X C D A B.
proof: Proof. unfold Perp_at. intros. spliter. repeat split. assumption. assumption. assumption. assumption. intros. apply l8_2. apply H3;assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR