simple one

Stream: new members

[BANGJI HU]

theorem anti_sym : ∀ x y : ℕ , x ≤ y → y ≤ x → x = y :=
begin
end

[BANGJI HU]

is it prooved in lean3?

[Scott Carnahan]

In the natural numbers game, this is inequality world level 6.

[edklencl]

@Scott Carnahancan you give me a github link?

[Scott Carnahan]

I am not so familiar with lean3, but I think you can find it with the PartialOrder instance on Nat.

[Matt Diamond]

In Lean3 it's docs3#nat.le_antisymm

[Matt Diamond]

not sure why you're asking about lean3 though...

[Michael Bucko]

Matt Diamond schrieb:

not sure why you're asking about lean3 though...

Shouldn't we forget about Lean3? (I only focus on Lean 4)