fact: Definition caseZ_diff (A : Type) (z : Z) (f : nat -> nat -> A) := match z with | Z0 => f 0 0 | Zpos m => f (nat_of_P m) 0 | Zneg m => f 0 (nat_of_P m) end.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid