lean: apportion's parts sum to the whole for any number of parts

The ranks of n parts are a permutation of 0..n-1 (being ahead is a strict
total order; pigeonhole by hand, core Lean has no subperm), so exactly
u parts get a unit and one gets the fraction. apportion_sum and
apportion_sum_of_shortfall; the audit shows only the standard axioms.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GWVo7x3UHw5kwCUaWxiejX

verify/lean/Audit.lean

@@ -32,3 +32,6 @@ open Wanderbooks
 #print axioms close_zeroes
 #print axioms close_credits_net_income
 #print axioms statements_add_up
+#print axioms Apportion.ranks_perm
+#print axioms Apportion.apportion_sum
+#print axioms Apportion.apportion_sum_of_shortfall