proposition: Lemma inj_min n m : 0<=n -> 0<=m -> Z.abs_N (Z.min n m) = N.min (Z.abs_N n) (Z.abs_N m).
proof: Proof. intros. rewrite !abs_N_nonneg; trivial. - now apply Z2N.inj_min. - now apply Z.min_glb. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat