proposition: Lemma mult_compat : forall n p, (F n) * (F p) = F (n * p)%nat.
proof: Proof. induction n; destruct p; simpl; auto. rewrite (mult_0_r n). compute; trivial. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List