proposition: Lemma mult_1_a : forall a, nf a -> (F 1) * a = a.
proof: Proof. induction a. simpl. trivial. simpl. simpl in IHa2. intro. caseEq a1. intro. subst a1. rewrite (nf_of_finite H). rewrite <- (plus_n_O n). auto. intros. subst a1. unfold finite in IHa2. rewrite IHa2. auto. nf_inv. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List