proposition: Lemma rmb_cong : forall A B C D, Rhombus A B C D -> Cong A B B C /\ Cong A B C D /\ Cong A B D A.
proof: Proof. intros. unfold Rhombus in H. spliter. assert(HH:= plg_to_parallelogram A B C D H). assert(HH1:= plg_cong A B C D HH). spliter. repeat split; trivial. apply cong_transitivity with B C; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates