proposition: Lemma Perp_perm : forall A B C D, Perp A B C D -> Perp A B C D /\ Perp B A C D /\ Perp A B D C /\ Perp B A D C /\ Perp C D A B /\ Perp C D B A /\ Perp D C A B /\ Perp D C B A.
proof: Proof. intros. repeat split; Perp. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR