proposition: Lemma ARgen_phiPOS_mult : forall x y, gen_phiPOS1 (x * y) == gen_phiPOS1 x * gen_phiPOS1 y.
proof: Proof. induction x;intros;simpl;norm. - rewrite ARgen_phiPOS_add;simpl;rewrite IHx;norm. - rewrite IHx;reflexivity. Qed.
imports: ZArith_base Zpow_def BinInt BinNat Setoid BinList BinPos BinNat BinInt Setoid Ncring Ncring_polynom