proposition: Lemma perp3__rect : forall A B C D, Perp A B B C -> Perp B C C D -> Perp C D D A -> Rectangle A B C D.
proof: Proof. intros A B C D. apply cop_perp3__rect, all_coplanar. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates