proposition: Lemma gen_phiZ_mul : forall x y, [x * y] == [x] * [y].
proof: Proof. intros x y;repeat rewrite same_genZ. destruct x;destruct y;simpl;norm; rewrite ARgen_phiPOS_mult;try (norm;fail). rewrite ring_opp_opp ;reflexivity. Qed.
imports: ZArith_base Zpow_def BinInt BinNat Setoid BinList BinPos BinNat BinInt Setoid Ncring Ncring_polynom