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