Fun 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.")

@lyxia Fun indeed! The moment when I did "Print Pos.add"... 😨

Took me 20 minutes in the end.

Sign in to participate in the conversation
La Quadrature du Net - Mastodon - Media Fédéré est une serveur Mastodon francophone, géré par La Quadrature du Net.