use int.Int
function sum_of_odd_numbers int : int
(** `sum_of_odd_numbers n` denote the sum of odd numbers from `1` to `2n-1` *)
axiom sum_of_odd_numbers_base : sum_of_odd_numbers 0 = 0
axiom sum_of_odd_numbers_rec : forall n. n >= 1 ->
sum_of_odd_numbers n = sum_of_odd_numbers (n-1) + 2*n - 1
goal sum_of_odd_numbers_1 : sum_of_odd_numbers 1 = 1
goal sum_of_odd_numbers_2 : sum_of_odd_numbers 2 = 4
goal sum_of_odd_numbers_3 : sum_of_odd_numbers 5 = 25
goal sum_of_odd_numbers_any: forall n. n >= 0 -> sum_of_odd_numbers n = n * n