proposition: Theorem Z_lt_abs_induction : forall P:Z -> Prop, (forall n:Z, (forall m:Z, Z.abs m < Z.abs n -> P m) -> P n) -> forall n:Z, P n.
proof: Proof. intros P HP p. set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *. enough (Q (Z.abs p)) as H by (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith). apply (Z_lt_induction Q); auto with zarith. subst Q; intros ? H. split; apply HP. - rewrite Z.abs_eq; auto; intros m ?. elim (H (Z.abs m)); intros; auto with zarith. elim (Zabs_dec m); intro eq; rewrite eq; trivial. - rewrite Z.abs_neq, Z.opp_involutive; [intros m ?|]. + destruct (H (Z.abs m)); auto with zarith. destruct (Zabs_dec m) as [-> | ->]; trivial. + apply Z.opp_le_mono; rewrite Z.opp_involutive; auto. Qed.
imports: ZArithRing ZArith_base Wf_nat