proposition: Lemma per_rmb : forall A B C D M, Plg A B C D -> Midpoint M A C -> Per A M B -> Rhombus A B C D.
proof: Proof. intros. unfold Per in H1. ex_and H1 D'. assert(HH:=H). unfold Plg in HH. spliter. ex_and H4 M'. assert(M = M'). eapply l7_17. apply H0. apply H4. subst M'. assert(D = D'). eapply symmetric_point_uniqueness. apply H5. assumption. subst D'. unfold Rhombus. split. assumption. assert(Cong A D B C). apply plg_to_parallelogram in H. assert(HH:=plg_cong A B C D H). spliter. assumption. eapply cong_transitivity. apply H2. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates