proposition: Lemma plg_per_rect3 : forall A B C D, Plg A B C D -> Per A D C -> Rectangle A B C D.
proof: Proof. intros. apply rect_permut. apply plg_per_rect1. apply parallelogram_to_plg. apply plg_to_parallelogram in H. apply plg_permut. apply plg_sym. assumption. apply l8_2. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates