proposition: Lemma cop_perp3__rect : 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 -> Rectangle A B C D.
proof: Proof. intros. assert (~ Col A B C) by (assert_diffs; apply per_not_col; Perp). assert (Par A B C D) by (apply (l12_9 A B C D B C); Perp; Cop). assert (Perp D A A B) by (eapply cop_perp3__perp;eauto). assert (Par A D B C) by (apply (l12_9 A D B C A B); Perp; Cop). assert (Parallelogram_strict A B C D) by (apply (parallel_2_plg); auto). apply plg_per_rect1. apply parallelogram_to_plg. apply Parallelogram_strict_Parallelogram. assumption. Perp. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates