proposition: Lemma Square_Parallelogram : forall A B C D, Square A B C D -> Parallelogram A B C D.
proof: Proof. intros. apply Square_Rectangle in H. apply Rectangle_Parallelogram in H. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel