proposition: Lemma Zcase_sign : forall (n:Z) (P:Prop), (n = 0 -> P) -> (n > 0 -> P) -> (n < 0 -> P) -> P.
proof: Proof. intros x P Hzero Hpos Hneg. destruct x; [apply Hzero|apply Hpos|apply Hneg]; easy. Qed.
imports: ZArithRing ZArith_base Wf_nat