proposition: Lemma string_compare_eq_refl : forall x, string_compare x x = Eq.
proof: Proof. intro x; induction x; simpl; trivial; autorewrite_nat_compare. trivial. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Strings.Ascii Coq.Structures.OrderedType Fiat.Common.Coq__8_4__8_5__Compat