proposition: Lemma RhombusEx: exists A B C D, Rhombus A B C D.
proof: Proof. destruct lower_dim_ex as [A [B [C HNC]]]. assert (H1 : ~ Col A B C) by auto. clear HNC. assert_diffs. assert (HAB := perp_bisect_existence A B); destruct HAB as [C1 [C2 HAB]]; try (assert_diffs; assumption). assert(Cong A C1 B C1). apply perp_bisect_cong_2 with C2. apply perp_bisect_sym_1. assumption. unfold Perp_bisect in HAB. spliter. unfold ReflectL in *. spliter. destruct H0 as [M H0]; spliter. assert(H10 := H). unfold Midpoint in H10. spliter. assert (exists x, Bet C1 M x /\ Cong M x C1 M) by (apply segment_construction). ex_and H8 x. exists A. exists C1. exists B. exists x. assert(Plg A C1 B x). unfold Plg. split. tauto. exists M. split. apply l7_2;assumption. unfold Midpoint. split. assumption. Cong. unfold Rhombus. split. assumption. Cong. Qed.
imports: GeoCoq.Tarski_dev.Annexes.perp_bisect