proposition: Lemma inj_max n m : Z.of_N (N.max n m) = Z.max (Z.of_N n) (Z.of_N m).
proof: Proof. unfold Z.max, N.max. rewrite inj_compare. case N.compare_spec; intros; subst; trivial. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat