The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Dear all,

Still, the theorem is not true. Executing the tactics

intros [[|] [|] [|] [|] [|] [|] [|] [|]];
   unfold upper, lower, nat_of_ascii, ascii_of_nat, ascii_of_pos;
   compute;
   try tauto.

leaves us with rather uprovable goals. Because you are adding first the problem is not in the lower range of the asciis but in the upper one.

All the best,
Chris