proposition: Lemma compare_antisym : forall s1 s2 : string, compare s1 s2 = CompOpp (compare s2 s1).
proof: Proof. induction s1, s2; intuition. simpl. rewrite Ascii.compare_antisym. destruct (Ascii.compare a0 a); simpl; intuition. Qed.
imports: Arith Ascii Bool Coq.Strings.Byte