proposition: Lemma gen_phiN_add : 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_add Rsth Reqe ARth). Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom