lemma_nat_align_down_within_block

vstd_extra::arithmetic

Function lemma_nat_align_down_within_block 

Source 
pub proof fn lemma_nat_align_down_within_block(x: nat, k1: nat, k2: nat)
Expand description
requires
k1 > 0,
k2 > 0,
k2 % k1 == 0,
ensures
nat_align_down(x, k1) + k1 <= nat_align_down(x, k2) + k2,

The finer-aligned block [align_down(x,k1), align_down(x,k1)+k1) fits inside the coarser-aligned block [align_down(x,k2), align_down(x,k2)+k2) when k1 divides k2.