proposition: Lemma big_number_eq : f (f 27 + 28) = 3 * 2 ^ (3 * 2 ^ (3 ^3) + 3 ^3) - 1.
proof: Proof. unfold f. rewrite <- pred_of_minus. replace 27 with (3^3). generalize (3^3). intro n; assert (0 < 2 ^ n). induction n. simpl;auto with arith. simpl. auto with arith. generalize H ; generalize (2 ^n). intros. replace (pred (3*n0) + S n) with (3*n0 + n). auto. omega. simpl;trivial. Qed.
imports: Arith Omega Relations