The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 12/11/2014 08:03, 
ncyms8r3x2 AT snkmail.com
 wrote:
> Let's say I have a function:
>      Definition f (x:R) := (x + 1)/(x - 1).
>
> Is there anyway to prove what that 1 isn't in its domain?

No, because 1 is in its domain. The logic of Coq (and of most other 
proof assistants) is a logic of total functions. Even if you can't prove 
anything interesting about f(1), it is nonetheless a real number.

If you want to forcibly remove 1 from the domain of f, you can define it 
as follows:

Definition f (x:R) (_: x <> 1) := (x + 1)/(x - 1).

Or as follows:

Definition f (x: {t:R | t <> 1}) := (projS1 x + 1)/(projS1 x - 1).

But I would strongly advise against it.

Best regards,

Guillaume