fact: Definition Zsum := fun n m f => if Zle_bool n m then iter 0 f Zplus (progression Z.succ n (Z.abs_nat ((1 + m) - n))) else iter 0 f Zplus (progression Z.pred n (Z.abs_nat ((1 + n) - m))).
imports: Arith ArithRing ListAux ZArith Lia Iterator ZProgression