proposition: Lemma Cdiff_Z_ind : forall P : Z -> CProp, (forall m n : nat, P (m - n)%Z) -> forall z : Z, P z.
proof: Proof. intros P H z. apply Cnats_Z_ind. intro n. replace (Z_of_nat n) with (n - 0%nat)%Z. apply H. simpl in |- *. auto with zarith. intro n. replace (- n)%Z with (0%nat - n)%Z. apply H. simpl in |- *. reflexivity. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)