proposition: Lemma inj_min n m : 0<=n -> 0<=m -> Z.abs_nat (Z.min n m) = Nat.min (Z.abs_nat n) (Z.abs_nat m).
proof: Proof. intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_min, N2Nat.inj_min. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat