proposition: Lemma inject_nat_S_inf : forall x : Z, (0 < x)%Z -> {n : nat | x = S n}.
proof: Proof. intros [| p| p] Hp; try discriminate Hp. exists (pred (nat_of_P p)). rewrite S_predn. symmetry in |- *; apply ZL9. clear Hp; apply sym_not_equal. apply Nat.neq_sym; apply Nat.neq_0_lt_0. apply lt_O_nat_of_P. Qed.
imports: Coq(Lia)