proposition: Theorem lt_not_eq : forall s1 s2 : string, lt s1 s2 -> ~ eq s1 s2.
proof: Proof. unfold lt, eq; induction s1 as [| c1 s1']. destruct s2; simpl; congruence. destruct s2 as [| c2 s2']; simpl. congruence. destruct (AsciiOT.compare c1 c2) as [? | ? | ?] eqn:?; intros Hc Heq; inversion Heq. subst; not_ascii_lt_refl. apply IHs1' in Hc; apply Hc; assumption. congruence. Qed.
imports: OrderedType Bool Ascii NArith Coq.Strings.String