proposition: Lemma exp_F_compat : forall p n, exp_F (F n) p = F (n ^ p)%nat.
proof: Proof. induction p;simpl. trivial. intro n. rewrite (IHp n). rewrite mult_compat; trivial. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List