Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Mon, 22 Aug 1994 13:32:57 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA09441;
          Mon, 22 Aug 1994 06:18:58 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from sun2.nsfnet-relay.ac.uk by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA09434;
          Mon, 22 Aug 1994 06:16:42 -0600
Via: uk.ac.warwick.eng; Mon, 22 Aug 1994 13:11:56 +0100
Received: from eng.warwick.ac.uk (falcon.eng.warwick.ac.uk) 
          by eagle.eng.warwick.ac.uk; Mon, 22 Aug 94 13:11:38 BST
From: es2033@eng.warwick.ac.uk
Message-Id: <24957.9408221211@eng.warwick.ac.uk>
Subject: Could anyone prove this for me?
To: info-hol@leopard.cs.byu.edu
Date: Mon, 22 Aug 94 13:11:39 BST
X-Mailer: ELM [version 2.3 PL8]


 Hi,

 I am trying to prove "!x. sqrt (x pow 2) = abs x" using library `reals`.

 Could anybody prove this?

 Nam - es2033@eng.warwick.ac.uk