proposition: Lemma cmp_lt (a b : string): cmp a b = Lt <-> lt a b.
proof: Proof. revert b. induction a as [ | a_head a_tail ], b; try easy; cbn. { split; trivial. intro. apply lts_empty. } remember (Ascii.compare _ _) as c eqn:Heqc. symmetry in Heqc. destruct c; split; intro H; try discriminate; trivial. { rewrite Ascii_as_OT.cmp_eq in Heqc. subst. apply String_as_OT.lts_tail. apply IHa_tail. assumption. } { rewrite Ascii_as_OT.cmp_eq in Heqc. subst. inversion H; subst. { rewrite IHa_tail. assumption. } exfalso. apply (Nat.lt_irrefl (nat_of_ascii a)). assumption. } { apply String_as_OT.lts_head. rewrite<- Ascii_as_OT.cmp_lt_nat. assumption. } { exfalso. inversion H; subst. { assert(X: Ascii.compare a a = Eq). { apply Ascii_as_OT.cmp_eq. trivial. } rewrite Heqc in X. discriminate. } rewrite<- Ascii_as_OT.cmp_lt_nat in *. unfold Ascii_as_OT.cmp in *. rewrite Heqc in *. discriminate. } Qed.
imports: OrderedType ZArith_base PeanoNat Peano_dec Compare_dec Ascii String NArith Ndec