proposition: Lemma perp_rmb : forall A B C D, Plg A B C D -> Perp A C B D -> Rhombus A B C D.
proof: Proof. intros. assert(HH:=midpoint_existence A C). ex_and HH M. apply (per_rmb A B C D M). assumption. assumption. apply perp_in_per. unfold Plg in H. spliter. ex_and H2 M'. assert(M = M'). eapply l7_17. apply H1. assumption. subst M'. assert(Perp A M B M). eapply perp_col. intro. subst M. apply is_midpoint_id in H1. subst C. apply perp_not_eq_1 in H0. tauto. apply perp_sym. eapply perp_col. intro. subst M. apply is_midpoint_id in H3. subst D. apply perp_not_eq_2 in H0. tauto. apply perp_sym. apply H0. unfold Midpoint in H3. spliter. apply bet_col in H3. Col. unfold Midpoint in H2. spliter. apply bet_col in H2. Col. apply perp_left_comm in H4. apply perp_perp_in in H4. apply perp_in_comm. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates