(P: Z -> Type): P 0 -> (forall n, 0 ≤ n -> P n -> P (1 + n)) -> forall n, 0 ≤ n -> P n. 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.
Require Import Import NatPair.Instances.