Theorem: MyNat.pred_succ (IIScExperiments/NatAddMul.lean)

State before:
a : MyNat
⊢ pred (succ a) = a
Tactic:
rfl
State after:
no goals