pub proof fn lemma_nat_align_down_monotone(x: nat, k1: nat, k2: nat)Expand description
requires
k1 > 0,k2 > 0,k2 % k1 == 0,nat_align_down(x, k2) <= nat_align_down(x, k1),nat_align_down(x, k2) % k1 == 0,When k2 is a multiple of k1, aligning to the coarser k2 gives a
value at most nat_align_down(x, k1): the k2-boundary is also a
k1-boundary, and it is the largest such boundary ≤ x.