for n, A, B, N being Nat st Fusc N = (A * (Fusc ((2 * n) + 1))) + (B * (Fusc (((2 * n) + 1) + 1))) holds
Fusc N = (A * (Fusc n)) + ((B + A) * (Fusc (n + 1)))