proposition: Lemma eq_Eq : forall x y, x = y -> string_compare x y = Eq.
proof: Proof. intros; subst; auto. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Strings.Ascii Coq.Structures.OrderedType Fiat.Common.Coq__8_4__8_5__Compat