The Coq mailing list

[vincent.chatel AT transport.alstom.com]

Hi everybody,

I would like to know if COQ supports the forward and backward proof in the 
same proof.
In other word, it is possible to build new hypothesis from the assumptions
and to make use of it to prove the goal.

thank for help

best regards

Vincent


:.________________
CONFIDENTIALITE : Ce message et les éventuelles pièces attachées sont
confidentiels. Si vous n'êtes pas dans la liste des destinataires, veuillez
informer l'expéditeur immédiatement et ne pas divulguer le contenu à une
tierce personne, ne pas l'utiliser pour quelque raison que ce soit, ne pas
stocker ou copier l'information qu'il contient sur un quelconque support.

CONFIDENTIALITY : This  e-mail  and  any attachments are confidential and
may be privileged. If  you are not a named recipient, please notify the
sender immediately and do not disclose the contents to another person, use
it for any purpose or store or copy the information in any medium.