// Some useful lemmas for non linear arithmetics
//@ lemma distr_right: forall x, y, z. x*(y+z) == (x*y)+(x*z) ;
//@ lemma distr_left: forall x, y, z. (x+y)*z == (x*z)+(y*z) ;


int isqrt(int n) {
  // When n is greater or equal to 0, the result should be the integer square root of n

  int count = 0;
  int sum = 1;
  while (sum <= n) {

    count++;
    sum = sum + 2*count+1;
  }
  return count;
}