(z : binnat): PropHolds (z <> 0) -> LeftCancellation (.*.) z. Proof. intros E. hnf in E. assert (H : unary z <> unary 0). { intros q. apply (equiv_inj unary) in q. exact (E q). } intros x y p. apply (ap unary) in p. rewrite <- unarymult, <- unarymult in p. exact (equiv_inj unary (nat_mult_cancel_l (unary z) H _ _ p)). Qed.
Require Import Require Import Require Import