lemma_nat_align_up_sound

vstd_extra::arithmetic

Function lemma_nat_align_up_sound 

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