proposition: Lemma rhombus_cong_square : forall A B C D, Rhombus A B C D -> Cong A C B D -> Square A B C D.
proof: Proof. intros. apply Rhombus_Rectangle_Square. assumption. apply Rhombus_Plg in H. apply plg_cong_rectangle;auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel