proposition: Lemma leb_antisym (a b : ascii) : leb a b = true -> leb b a = true -> a = b.
proof: Proof. unfold leb. rewrite compare_antisym. destruct (compare b a) eqn:Hcmp; simpl in *; intuition. - apply compare_eq_iff in Hcmp. intuition. - discriminate H. - discriminate H0. Qed.
imports: Bool BinPos BinNat PeanoNat Nnat Coq.Strings.Byte