forall z : nat, PropHolds (~ (z =N= 0)) -> LeftCancellation@{N} (.*.) z. Proof. unfold PropHolds. unfold LeftCancellation. intros a Ea b c E;revert b c a Ea E. induction b as [|b IHb];intros [|c];simpl_nat;intros a Ea E. - reflexivity. - rewrite mul_0_r in E. rewrite mul_S_r in E;apply symmetry in E. apply plus_eq_zero in E. destruct (Ea (fst E)). - rewrite mul_0_r,mul_S_r in E. apply plus_eq_zero in E. destruct (Ea (fst E)). - rewrite 2!mul_S_r in E. apply (left_cancellation _ _) in E. apply ap. apply IHb with a;trivial. Qed.
Require Import