proposition: Lemma Perp_cases : forall 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 -> Perp A B C D.
proof: Proof. intros. decompose [or] H; Perp. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR