proposition: Lemma lt_not_eq : forall x y, lt x y -> ~ eq x y.
proof: Proof. unfold lt, not in *; intros; rewrite Eq_eq_iff in *; exfalso_from_equalities. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Strings.Ascii Coq.Structures.OrderedType Fiat.Common.Coq__8_4__8_5__Compat