proposition: Lemma Z_of_nat_plus1 : forall n, Z_of_nat (1 + n) = Z.succ (Z_of_nat n).
proof: Proof. Proof using. intros. rewrite <- Z_of_nat_S. fequals~. Qed.
imports: Coq.ZArith.ZArith TLC(LibTactics LibLogic LibReflect LibRelation)