lemma_nat_align_down_sound

vstd_extra::arithmetic

Function lemma_nat_align_down_sound 

Source 
pub broadcast proof fn lemma_nat_align_down_sound(x: nat, align: nat)
Expand description
requires
align > 0,
ensures
#[trigger] nat_align_down(x, align) <= x,
nat_align_down(x, align) % align == 0,
forall |n: nat| n <= x && #[trigger] (n % align) == 0 ==> n <= nat_align_down(x, align),
x - nat_align_down(x, align) < align,