proposition: Lemma induction_nonneg (P: Z -> Type): P 0 -> (forall n, 0 ≤ n -> P n -> P (1 + n)) -> forall n, 0 ≤ n -> P n.
proof: Proof. intros P0 PS. refine (induction _ _ _ _); auto. intros n E1 ? E2. destruct (rings.is_ne_0 1). apply (antisymmetry (≤)). - apply (order_reflecting ((n - 1) +)). rewrite <-plus_assoc,plus_negate_l,2!plus_0_r. transitivity 0;trivial. - transitivity (n - 1);trivial. apply (order_reflecting (1 +)). rewrite plus_comm,<-plus_assoc,plus_negate_l,plus_0_r. transitivity 0. + trivial. + apply le_0_2. 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