An F* program for computing factorial sums

Factorial.fst

module Factorial

open FStar.Mul  // Give us * for multiplication instead of pairs
open FStar.IO
open FStar.Printf

let rec factorial (n:nat) : nat =
  if n = 0 then 1
  else n * factorial (n-1)

let rec sum (min:nat) (max:nat) (f:nat -> nat) : Tot nat (decreases max) =
  if max < min then 0
  else if max = min then f( min )
  else (f max) + sum min (max-1) f

let rec sum_of_factorial_aux (n:nat) (k:nat{ k <= n}) (k_factorial:nat) (accum:nat): Tot nat (decreases (n-k))
  = if k = n then accum + k_factorial
    else sum_of_factorial_aux n (k+1) ((k+1) * k_factorial) (accum + k_factorial)

let rec sum_of_factorial_lemma (n:nat) (k:nat{k <= n && 1 <= k})
   : Lemma (ensures sum_of_factorial_aux n k (factorial k) (sum 1 (k-1) factorial) =
                    (sum 1 n factorial))
                    (decreases (n-k))
   = if n = k
     then ()
     else sum_of_factorial_lemma n (k+1)     
  
val sum_of_factorials (n:nat{n >= 1}) : Tot (x:nat{x == sum 1 n factorial})
let sum_of_factorials n =
   sum_of_factorial_lemma n 1;
   sum_of_factorial_aux n 1 1 0

let _ = 
   let n = input_int() in
     if n >= 1 then
       print_string (sprintf "%d\n" (sum_of_factorials n))
     else
       print_string "Bad input\n"