(z:binnat) : LeftCancellation plus z. Proof. intros x y p. apply (equiv_inj unary). apply (ap unary) in p. rewrite <- unaryplus, <- unaryplus in p. exact (left_cancellation _ _ _ _ p). Qed.
Require Import Require Import Require Import