Theorem Nat.fib_succ_eq_succ_sum

Modification history