proposition: Lemma square_perp_rectangle : forall A B C D, Rectangle A B C D -> Perp A C B D -> Square A B C D.
proof: Proof. intros. assert (Rhombus A B C D). apply perp_rmb. apply H. assumption. apply Rhombus_Rectangle_Square;auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates