proposition: Lemma nat_compare_eq_refl : forall x, Nat.compare x x = Eq.
proof: Proof. intros; apply Nat.compare_eq_iff; trivial. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Strings.Ascii Coq.Structures.OrderedType Fiat.Common.Coq__8_4__8_5__Compat