proposition: Lemma proper_caseZ_diff : forall (A : Type) (f : nat -> nat -> A), (forall m n p q : nat, m + q = n + p -> f m n = f p q) -> forall m n : nat, caseZ_diff (m - n) f = f m n.
proof: Proof. intros A F H m n. pattern m, n in |- *. apply nat_double_ind. intro n0. replace (0%nat - n0)%Z with (- n0)%Z. rewrite caseZ_diff_Neg. reflexivity. simpl in |- *. reflexivity. intro n0. replace (S n0 - 0%nat)%Z with (Z_of_nat (S n0)). rewrite caseZ_diff_Pos. reflexivity. simpl in |- *. reflexivity. intros n0 m0 H0. rewrite (H (S n0) (S m0) n0 m0). rewrite <- H0. replace (S n0 - S m0)%Z with (n0 - m0)%Z. reflexivity. repeat rewrite Znat.inj_S. auto with zarith. auto with zarith. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid