proposition: Lemma eqb_spec (a b : ascii) : reflect (a = b) (a =? b)%char.
proof: Proof. destruct a, b; simpl. do 8 (case Bool.eqb_spec; [ intros -> | constructor; now intros [= ] ]). now constructor. Qed.
imports: Bool BinPos BinNat PeanoNat Nnat Coq.Strings.Byte