nat.smul_one_eq_coe for enat

Stream: Is there code for X?

[Yaël Dillies]

Is nat.smul_one_eq_coe really general enough? It doesn't apply here.

example (a : ℕ) : a • (1 : enat) = a :=

and has anybody a proof of that?

[Yaël Dillies]

Ahah! I think there's something fishy here. If you rw nsmul_one, you end up with the goal ↑a = ↑a. The LHS is nat.cast while the RHS is the coercion defined by instance : has_coe ℕ enat := ⟨some⟩ in data.nat.enat.

[Ryan Lahfa]

Yaël Dillies said:

Ahah! I think there's something fishy here. If you rw nsmul_one, you end up with the goal ↑a = ↑a. The LHS is nat.cast while the RHS is the coercion defined by instance : has_coe ℕ enat := ⟨some⟩ in data.nat.enat.

Does rw_mod_cast help?