where did I go classical?

Stream: general

[Kenny Lau]

theorem aux3 (n : nat) (H1 : ¬n < 3) (H2 : even n) : aux (n - 2) < aux n :=
begin
  have H3 := le_of_not_gt H1,
  rw [aux, aux, if_neg H1, if_pos H2],
  let m := n - 3,
  have H4 : n = m + 3,
  { dsimp [m], rw [nat.sub_add_cancel H3] },
  rw H4 at *,
  rw nat.add_sub_assoc,
  rw nat.add_sub_assoc,
  rw nat.add_sub_assoc,
  { simp,
    by_cases m + 1 < 3,
    { simp [h],
      apply add_lt_add_left,
      exact dec_trivial },
    { simp [h, even_of_even_add_two _ H2],
      apply nat.lt_add_of_pos_right,
      exact dec_trivial } },
  exact dec_trivial,
  exact dec_trivial,
  exact dec_trivial
end

[Kenny Lau]

this isn't MWE. I would understand if you can't read it off the lines

[Kenny Lau]

(it matters in this context, not because I'm a constructivist, it has nothing to do with my constructivism, I really need this to be constructive)

[Kenny Lau]

I suspect it's the dec_trivial, but natural inequality should be decidable

[Kenny Lau]

update: I removed every dec_trivial and proved the inequalities using constructor, it's still classical

[Gabriel Ebner]

It's le_of_not_gt, of course.

[Kenny Lau]

oh, how do I fix it?

[Gabriel Ebner]

If you really, really don't want classical logic, then you should probably prove a specialized version of le_of_not_gt for decidable linear orders.

[Kenny Lau]

is there no simple fix for naturals

[Johannes Hölzl]

Why do you need this as a constructive proof? There is no computable content.
You can constructively prove le_of_not_gt for nat using the decidability of lt on natural numbers.

[Kenny Lau]

because the content is outside

[Kenny Lau]

this is just a part

[Johannes Hölzl]

But rewriting ¬n < 3 to n <= 3 is not a problem for decidability in Lean. You are fine as long as only your proofs are classical.

[Kenny Lau]

oh and for the sake of completeness, the final product is here https://github.com/kckennylau/Lean/blob/master/recursion.lean