proposition: Lemma Nwscal_ok : forall n x, gen_phiNword (Nwscal n x) == gen_phiN rO rI radd rmul n * gen_phiNword x.
proof: Proof. intros n x; induction x as [|a x IHx]; intros. - norm. - simpl Nwscal. repeat rewrite gen_phiNword_cons. rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth)) by (destruct Reqe; constructor; trivial). rewrite IHx. norm. Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom