proposition: Lemma leb_antisym (s1 s2 : string) : leb s1 s2 = true -> leb s2 s1 = true -> s1 = s2.
proof: Proof. unfold leb. rewrite compare_antisym. destruct (compare s2 s1) eqn:Hcmp; simpl in *; intuition. - apply compare_eq_iff in Hcmp. intuition. - discriminate H. - discriminate H0. Qed.
imports: Arith Ascii Bool Coq.Strings.Byte