The Coq mailing list

[Marcus Ramos <mvmramos AT gmail.com>]

Hi,

This is probably a very basic question, but since I have no teacher to ask about, I guess whether any of you would give me a hint on how to prove the following theorem (a reduced version of the problem I am working with):

Require Import Ascii.

Definition upper (c: ascii): ascii := ascii_of_nat ((nat_of_ascii c)-32).

Definition lower (c: ascii): ascii := ascii_of_nat ((nat_of_ascii c)+32).

Theorem t:

   forall c: ascii,

   upper (lower c) = c.

It has to do with proving by induction over ascii, but I have no idea on how to do it. Once again, sorry for bothering with basic questions...

Thanks in advance,

Marcus.