proofs in cocalc

Stream: maths

[Jane]

Hey guys, can someone please help me with two problem using some of the axioms?

def has_min_element {A : Type} (R : A → A → Prop) : Prop :=
    ∃ x, ∀ y, R x y
axiom ax1 {n m: ℕ} : (n ≤ m) ↔ (∃ l : ℕ, n + l = m)
axiom ax2 {m n x y: ℕ} (h1 : x + n = y) (h2 : y + m = x): x = y ∧ (m = 0) ∧ (n = 0)
axiom ax3 {m n x y z : ℕ} (h1 : x + n = y) (h2 : y + m = z) : x + (n + m) = z
axiom ax4 : 1 ≠ 2
axiom ax5 (m n : ℕ) : ∃ l : ℕ, m + l = n ∨ n + l = m
axiom ax6 (n : ℕ) : 0 + n = n

theorem le_not_symmetric : ¬ (symmetric nat.less_than_or_equal) :=
sorry

example : ¬ (equivalence nat.less_than_or_equal) :=
sorry

Thank you guys soooo much !!!

[Anne Baanen]

To get started, it's good to realize ¬ p is the same as p → false, and x ≠ y is the same as ¬ (x = y), which is the same as (x = y) → false.

[Kevin Buzzard]

A lot of these axioms are things which one can prove in Lean anyway. Here's an axiom-free proof of the first one:

theorem le_not_symmetric : ¬ (symmetric nat.less_than_or_equal) :=
begin
  intro h, -- proof by "mathematician's contradiction", i.e. assume it's symmetric
  -- and get a contradiction
  unfold symmetric at h, -- says x ≤ y → y ≤ x
  have h12 : 1 ≤ 2 := dec_trivial,
  have h21 : ¬ 2 ≤ 1 := dec_trivial,
  apply h21,
  apply h,
  exact h12,
end

but it's hard to work out if this is what you're looking for.