proposition: Theorem lt_trans : forall s1 s2 s3 : string, lt s1 s2 -> lt s2 s3 -> lt s1 s3.
proof: Proof. unfold lt; intros s1 s2; generalize dependent s1; induction s2 as [| c2 s2']. destruct s1; [trivial | simpl; congruence]. destruct s1 as [| c1 s1']; simpl. destruct s3; [congruence | trivial]. destruct s3 as [| c3 s3']; [congruence |]. destruct (AsciiOT.compare c1 c2) as [? | ? | ?] eqn:?; destruct (AsciiOT.compare c2 c3) as [? | ? | ?] eqn:?; destruct (AsciiOT.compare c1 c3) as [? | ? | ?] eqn:?; unfold AsciiOT.eq in *; subst; solve [ apply IHs2' | congruence | repeat (try not_ascii_lt_refl; do_ascii_lt_trans) ]. Qed.
imports: OrderedType Bool Ascii NArith Coq.Strings.String