for a, b, k, l, n being Nat st n = ((a,b) In_Power (k + l)) . (k + 1) & l > 0 holds
a divides n