/*@

inductive nat = zero | succ(nat);

fixpoint int int_of_nat(nat n) {
    switch (n) {
        case zero: return 0;
        case succ(n0): return 1 + int_of_nat(n0);
    }
}

fixpoint nat nat_of_int(int n);

lemma_auto(int_of_nat(nat_of_int(n))) void int_of_nat_of_int(int n);
    requires 0 <= n;
    ensures int_of_nat(nat_of_int(n)) == n;
    
lemma_auto void nat_of_int_of_nat(nat n);
    requires true;
    ensures nat_of_int(int_of_nat(n)) == n;

lemma_auto void int_of_nat_nonnegative(nat n);
    requires true;
    ensures 0 <= int_of_nat(n);
    
lemma_auto void nat_of_int_zero();
  requires true;
  ensures nat_of_int(0) == zero;
  
lemma_auto(succ(nat_of_int(x))) void succ_int(int x);
  requires 0 <= x;
  ensures nat_of_int(x + 1) == succ(nat_of_int(x));
  
fixpoint nat prev(nat n){
  switch(n) {
    case zero: return zero;
    case succ(n0): return n0;
  }
} 

lemma void minuslemma(int x, int y);
  requires 0 < x && x <= y;
  ensures succ(nat_of_int(y - x)) == nat_of_int(y - int_of_nat(prev(nat_of_int(x))));


@*/