proposition: Lemma induction (P: Z -> Type): P 0 -> (forall n, 0 ≤ n -> P n -> P (1 + n)) -> (forall n, n ≤ 0 -> P n -> P (n - 1)) -> forall 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. + rewrite rings.preserves_0. trivial. + intros m E. rewrite rings.preserves_plus, rings.preserves_1. apply Psuc1. * apply to_semiring_nonneg. * trivial. - rewrite <-(groups.negate_involutive n), <-A. clear A. revert a. apply naturals.induction. + rewrite rings.preserves_0, rings.negate_0. trivial. + intros m E. rewrite rings.preserves_plus, rings.preserves_1. rewrite rings.negate_plus_distr, commutativity. apply Psuc2. * apply naturals.negate_to_ring_nonpos. * trivial. Qed.
imports: HoTT.Classes.implementations.peano_naturals HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.naturals HoTT.Classes.interfaces.orders HoTT.Classes.implementations.natpair_integers HoTT.Classes.theory.rings HoTT.Classes.theory.integers HoTT.Classes.orders.nat_int