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 ARth);try (norm;fail). rewrite (Ropp_opp Rsth Reqe Rth);rrefl. Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom