proposition: Lemma phi0_plus_mult : forall a b, nf a -> nf b -> phi0 (a + b) = phi0 a * phi0 b.
proof: Proof. cbn; intro a; case a. - intro b; case b;reflexivity. - intros until b;case b;simpl. + case alpha;cbn;auto. + reflexivity. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)