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