protected_test.lean.expected.out

protected_test.lean:2:9: error: unknown identifier 'induction_on'
protected_test.lean:3:9: error: unknown identifier 'rec_on'
less_than_or_equal.rec_on :
  ?M_1.less_than_or_equal ?M_3 →
  ?M_2 ?M_1 → (∀ {b : ℕ}, ?M_1.less_than_or_equal b → ?M_2 b → ?M_2 b.succ) → ?M_2 ?M_3
less_than_or_equal.rec_on :
  ?M_1.less_than_or_equal ?M_3 →
  ?M_2 ?M_1 → (∀ {b : ℕ}, ?M_1.less_than_or_equal b → ?M_2 b → ?M_2 b.succ) → ?M_2 ?M_3
protected_test.lean:7:11: error: unknown identifier 'rec_on'
less_than_or_equal.rec_on :
  ?M_1.less_than_or_equal ?M_3 →
  ?M_2 ?M_1 → (∀ {b : ℕ}, ?M_1.less_than_or_equal b → ?M_2 b → ?M_2 b.succ) → ?M_2 ?M_3