x / x = 1

Stream: new members

[Julian Berman]

What do I need to be able to prove:

example {P : Type} [fintype P] [nonempty P] : fintype.card P / fintype.card P = 1 := sorry

Am I using nonempty incorrectly?

[Mario Carneiro]

Is that nat division?

[Julian Berman]

I think so if I understand #check fintype.card telling me it returns a natural

[Julian Berman]

do I need some : R's?

[Mario Carneiro]

(by which I mean, it is, but are you sure you want to be using it)

[Mario Carneiro]

It's true either way, but it might be less useful than you intend, depending on what you are using this for

[Mario Carneiro]

The proof breaks down into x != 0 -> x / x = 1 and nonempty P -> fintype.card P != 0

[Julian Berman]

Ah, sorry -- no I want division in R.. sec, pasting my code

[Mario Carneiro]

In that case, it breaks down into (x:real) != 0 -> x/x = 1, (x:real) = 0 <-> x = 0 and the last thing

[Julian Berman]

Got it think I follow, thanks! Will give that a shot.