proposition: Lemma cmp_antisym (a b : string): cmp a b = CompOpp (cmp b a).
proof: Proof. revert b. induction a, b; try easy. cbn. rewrite IHa. clear IHa. remember (Ascii.compare _ _) as c eqn:Heqc. symmetry in Heqc. destruct c; rewrite Ascii_as_OT.cmp_antisym in Heqc; destruct Ascii_as_OT.cmp; cbn in *; easy. Qed.
imports: OrderedType ZArith_base PeanoNat Peano_dec Compare_dec Ascii String NArith Ndec