proposition: Lemma exp_compat : forall p n, (F n) ^ (F p) = F (n ^ p)%nat.
proof: Proof. induction p. destruct n;simpl. auto. destruct n;auto. destruct n;simpl. auto. case n. simpl. rewrite power_of_1. rewrite <- plus_n_O;auto. simpl. intros. replace (cons zero (S n0) zero) with (finite (S (S n0))). 2:simpl;auto. rewrite exp_F_compat. rewrite mult_compat. assert ( (S (S n0) * S (S n0) ^ p) = (S (S n0) ^ p + (S (S n0) ^ p + n0 * S (S n0) ^ p)))%nat. ring. rewrite H;trivial. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List