proposition: Lemma rect_comm2 : forall A B C D, Rectangle A B C D -> Rectangle B A D C.
proof: Proof. intros. unfold Rectangle in *. spliter. apply plg_to_parallelogram in H. apply plg_comm2 in H. split. apply parallelogram_to_plg. assumption. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates