proposition: Lemma rmb_perp : forall A B C D, A <> C -> B <> D -> Rhombus A B C D -> Perp A C B D.
proof: Proof. intros. assert(HH:= H1). unfold Rhombus in HH. spliter. apply plg_to_parallelogram in H2. apply plg_mid in H2. ex_and H2 M. assert(HH:= H1). eapply (rmb_per _ _ _ _ M) in HH. apply per_perp_in in HH. apply perp_in_perp_bis in HH. induction HH. apply perp_not_eq_1 in H5. tauto. unfold Midpoint in *. spliter. eapply perp_col. assumption. apply perp_sym. apply perp_left_comm. eapply perp_col. auto. apply perp_left_comm. apply perp_sym. apply H5. apply bet_col in H4. Col. apply bet_col in H2. Col. intro. subst M. apply is_midpoint_id in H2. contradiction. intro. subst M. apply l7_2 in H4. apply is_midpoint_id in H4. subst D. tauto. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates