proposition: Lemma induction (P: Z → Prop) `{!Proper ((=) ==> iff) P}: P 0 → (∀ n, 0 ≤ n → P n → P (1 + n)) → (∀ n, n ≤ 0 → P n → P (n - 1)) → ∀ n, P n.
proof: Proof. intros P0 Psuc1 Psuc2 n. destruct (int_abs_sig Z nat n) as [[a A]|[a A]]. rewrite <-A. clear A. revert a. apply naturals.induction. solve_proper. now rewrite rings.preserves_0. intros m E. rewrite rings.preserves_plus, rings.preserves_1. apply Psuc1. apply to_semiring_nonneg. easy. rewrite <-(groups.negate_involutive n), <-A. clear A. revert a. apply naturals.induction. solve_proper. now rewrite rings.preserves_0, rings.negate_0. intros m E. rewrite rings.preserves_plus, rings.preserves_1. rewrite rings.negate_plus_distr, commutativity. apply Psuc2. apply naturals.negate_to_ring_nonpos. easy. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.naturals MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.implementations.natpair_integers MathClasses.orders.rings MathClasses.orders.nat_int