proposition: Lemma rect_per : forall A B C D, Rectangle A B C D -> Per B A D /\ Per A B C /\ Per B C D /\ Per A D C.
proof: Proof. intros. repeat split. apply (rect_per1 A B C D); assumption. apply (rect_per2 A B C D); assumption. apply (rect_per3 A B C D); assumption. apply (rect_per4 A B C D); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates