Fun #coq challenge by Talia Ringer on twitter:
How fast can you prove
N.succ (N.add x y) = N.add x (N.succ y)
without stdlib lemmas? As in, pretend you only just defined N and its operations.
NB: this is the binary N, not the unary nat, so it's a bit trickier than it looks.
(The starting import is "From Coq Require Import NArith.")
Mamot.fr est une serveur Mastodon francophone, géré par La Quadrature du Net.