Thrithralas

import Mathlib.Tactic.Common

theorem Nat.nmd_aux (f : ℕ → ℕ) : (∀ n k, n < k → f n > f k) → ∀ k, f k + k ≤ f 0 := by
  intro pr k
  induction' k with k ih
  . apply Nat.le.refl
  . trans
    swap
    . exact ih
    . nth_rw 2 [Nat.add_comm k 1]

Thrithralas

MyEnum e = MyEnum.ME1;

for (int i = 0; i < 4; i++) {
   e = (MyEnum) ((int) (e + 1) & 3);
   System.Console.WriteLine(e);
}


public enum MyEnum {
    ME1,