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