proposition: Lemma caseZ_diff_Pos : forall (A : Type) (f : nat -> nat -> A) (n : nat), caseZ_diff n f = f n 0.
proof: Proof. intros A f n. elim n. reflexivity. intros n0 H. simpl in |- *. rewrite nat_of_P_o_P_of_succ_nat_eq_succ. reflexivity. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid