axiom distr_left : forall a,b,c:int. a * (b+c) = a*b + a*c
axiom distr_right: forall a,b,c:int. (b+c) * a = b*a + c*a

let sum (n:int) =
  { n>=0 }
  let i = ref 0 in
  let s = ref 0 in
  begin
    while !i < n do
      { invariant 2*s = i*(i+1)  and  i<=n
        variant n-i }
      i := !i + 1;
      s := !s + !i
    done;
    !s
  end
  { 2*result = n*(n+1) }