proposition: Lemma cop_perp3__perp : forall A B C D, Coplanar A B C D -> Perp A B B C -> Perp B C C D -> Perp C D D A -> Perp D A A B.
proof: Proof. intros. assert (Par A B C D) by (apply (l12_9 A B C D B C); Perp; Cop). assert (Perp A B D A) by (apply (cop_par_perp__perp C D A B D A); Perp; Par; Cop). auto using perp_sym, perp_left_comm. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates