fact: Fixpoint exp_F (a:T1)(n:nat){struct n}:T1 := match n with | 0 => F 1 | S p => a * (exp_F a p) end.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List