proposition: Lemma plg_per_rect : forall A B C D, Plg A B C D -> (Per D A B \/ Per C B A \/ Per A D C \/ Per B C D) -> Rectangle A B C D.
proof: Proof. intros. induction H0. apply plg_per_rect1; assumption. induction H0. apply plg_per_rect2; assumption. induction H0. apply plg_per_rect3; assumption. apply plg_per_rect4; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates