proposition: Lemma phi0_plus_mult : forall a b, nf a -> nf b -> phi0 (a + b) = phi0 a * phi0 b.
proof: Proof. simpl. intro a; case a. intro b; case b;simpl. compute;trivial. compute; trivial. intros until b;case b;simpl. case t;simpl;auto. intro H; rewrite (nf_of_finite H). compute;trivial. case t;simpl. compute;auto. unfold phi0;auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List