proposition: Lemma inj_min n m : Z.to_N (Z.min n m) = N.min (Z.to_N n) (Z.to_N m).
proof: Proof. destruct n, m; simpl; trivial; unfold Z.min, N.min; simpl; now case Pos.compare. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat