proposition: Lemma RhombusUnicity: forall A B C D E, Rhombus A B C D -> Rhombus A B C E -> D = E.
proof: Proof. intros. unfold Rhombus in *. spliter. unfold Plg in *. spliter. ex_and H4 M. ex_and H3 N. assert (M = N). apply l7_17 with A C;assumption. subst. apply symmetric_point_uniqueness with B N;assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.perp_bisect