proposition: Lemma Square_Rhombus : forall A B C D, Square A B C D -> Rhombus A B C D.
proof: Proof. intros. unfold Rhombus. split. apply Square_Parallelogram in H. apply parallelogram_to_plg in H. assumption. unfold Square in H. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates