Binary Nat thing from https://twitter.com/TaliaRinger/status/1370213824716963840

BinaryNatTest.agda

open import Data.Nat.Binary
open import Relation.Binary.PropositionalEquality

plus-zero : ∀ n -> (n + zero) ≡ n
plus-zero zero = refl
plus-zero 2[1+ n ] = refl
plus-zero 1+[2 n ] = refl


plus-suc : ∀ n m -> suc (n + m) ≡ n + (suc m)
plus-suc zero m = refl
plus-suc 2[1+ n ] zero rewrite plus-zero n  = refl
plus-suc 1+[2 n ] zero rewrite plus-zero n = refl
plus-suc 2[1+ n ] 2[1+ m ] rewrite plus-suc n m = refl
plus-suc 2[1+ n ] 1+[2 m ]  = refl
plus-suc 1+[2 n ] 2[1+ m ] rewrite plus-suc n m  = refl
plus-suc 1+[2 n ] 1+[2 m ] = refl