proposition: Lemma induction_nonneg (P: Z → Prop) `{!Proper ((=) ==> iff) P}: P 0 → (∀ n, 0 ≤ n → P n → P (1 + n)) → ∀ n, 0 ≤ n → P n.
proof: Proof. intros P0 PS. refine (induction _ _ _ _); auto. solve_proper. intros n E1 ? E2. destruct (rings.is_ne_0 1). apply (antisymmetry (≤)). apply (order_reflecting ((n - 1) +)). ring_simplify. now transitivity 0. transitivity (n - 1). easy. apply (order_reflecting (1 +)). ring_simplify. transitivity 0. easy. apply semirings.le_0_2. 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