Exp.leon.scala

import leon.lang._
import leon.collection._
import leon._

object Test {
  def exp(a: BigInt, i: BigInt): BigInt = {
    require(i>=0)
    
    if (i == 0) 1
    else a * exp(a, i-1)
  }
  
  def lemma(a: BigInt, i: BigInt, j: BigInt): Boolean = {
    require(i >= 0 && j >= 0)
    
    exp(a, i+j) == exp(a, i) * exp(a, j) && {
      if (j == 0) true
      else lemma(a, i, j-1) 
    }
  }.holds
  
  
}