proposition: Theorem succ_ne_zero (a : mynat) : succ a ≠ 0.
proof: Proof. intro f. apply (zero_ne_succ a). symmetry. exact f. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.World.Addition Game.World.Proposition Game.World.AdvancedProposition Setoid