proposition: Lemma Zabs_nat_le n m : 0 <= n <= m -> (Z.abs_nat n <= Z.abs_nat m)%nat.
proof: Proof. intros (H,H'). apply Zabs2Nat.inj_le; trivial. now transitivity n. Qed.
imports: Arith_base BinPos BinInt Zcompare Zorder Znat ZArith_dec