fact: Definition alessthan (a: aexp) (v: Z) : assertion := fun (s: store) => 0 <= aeval a s < v.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)