(m n : nat) : binary m + binary n = binary (m + n). Proof. induction m; induction n; try reflexivity. - simpl. rewrite binnatplussucc. apply ap. done. - simpl. rewrite <- IHm. rewrite binnatplussucc. done. Qed.
Require Import Require Import Require Import