Function div_ensures Copy item path

pub uninterp fn div_ensures<A>(x: A, y: A, o: A) -> bool