(m n : binnat) : unary m + unary n = unary (m + n). Proof. etransitivity (unary (binary (_^-1 m + _^-1 n))). - apply ((eissect binary (unary m + unary n)) ^). - rewrite <- binaryplus. rewrite (eisretr binary m), (eisretr binary n). reflexivity. Qed.
Require Import Require Import Require Import