import MyNat.Definition

Tactic : rw

The rw tactic is simply the rewrite tactic followed by rfl.

See rewrite for more details.

See rfl for more details.