proposition: Lemma Cnats_Z_ind : forall P : Z -> CProp, (forall n : nat, P n) -> (forall n : nat, P (- n)%Z) -> forall z : Z, P z.
proof: Proof. intros P H H0 z. elim (CZ_exh z); intros H1. elim H1; intros n H2. rewrite H2. apply H. elim H1; intros n H2. rewrite H2. apply H0. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)