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