proposition: Lemma Rectangle_Parallelogram : forall A B C D, Rectangle A B C D -> Parallelogram A B C D.
proof: Proof. unfold Rectangle. intros. decompose [and] H. apply plg_to_parallelogram in H0. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel