proposition: Lemma Zabs_ind : forall (P:Z -> Prop) (n:Z), (n >= 0 -> P n) -> (n <= 0 -> P (- n)) -> P (Z.abs n).
proof: Proof. intros. apply Z.abs_case_strong; Z.swap_greater; trivial. intros x y Hx; now subst. Qed.
imports: Arith_base BinPos BinInt Zcompare Zorder Znat ZArith_dec