proposition: Lemma rect_per2 : forall A B C D, Rectangle A B C D -> Per A B C.
proof: Proof. intros. apply rect_comm2 in H. eapply rect_per1. apply H. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates