proposition: Theorem Z2Nat_id_max : ∀ x, Z.of_nat (Z.to_nat x) = Z.max 0 x.
proof: Proof. intros x. destruct x as [| x| x]; [ reflexivity | idtac | reflexivity ]. rewrite Z2Nat.id; [ reflexivity | apply Pos2Z.is_nonneg ]. Qed.
imports: Utf8 QArith NPeano Sorted Psatz