proposition: Lemma gen_phiN_mult : forall x y, [x * y] == [x] * [y].
proof: Proof. intros x y;repeat rewrite same_genN. destruct x;destruct y;simpl;norm. apply (ARgen_phiPOS_mult Rsth Reqe ARth). Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom