introducing a weird less-than symbol

Stream: new members

[Michael Beeson]

I need two kinds of less-than, so I have to introduce a new symbol for one of them, and I tried to make it \le\H where \H produces H in mathbb. So I made a typographical error that Reid Barton pointed out, and would delete this
post except I was told not to delete posts as they might still be useful. Thanks Reid. The example below is
fixed now.

reserve infix ` ≤ℍ `: 49
reserve infix ` <ℍ `: 49

class  Model (M:Type) :=
(𝔽:M)
(𝕊:M → M)  --successor
(zero:M)
(mem:M → M → Prop)
(addition: M → M → M)
(le: M → M → Prop)
(leH: M → M → Prop)
(lessthan: M → M → Prop)
(lessthanH: M → M → Prop)
(infix  ∈ :=  mem )
(infix  + := addition)
(additive_identity: ∀ x, x ∈ 𝔽 →  x + zero = x)
(leH_definition: ∀ x y, (leH x y ↔ ∃ k, x + k = y))
(lessthanH_definition: ∀ x y, (lessthanH x y ↔ ∃ k, x + 𝕊 k = y))

variables (M:Type) [Model M] (a b x y z u v w X R W: M)

open Model
infix + := addition
infix  ≤ℍ := leH
infix  <ℍ := lessthanH

lemma test3: ∀ (x:M), x + zero ≤ℍ x:=
  begin

  end

[Reid Barton]

I think you wanted to define infix <ℍ := lessthanH