proposition: Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y].
proof: Proof. intros x y; repeat rewrite same_genZ; generalize x y;clear x y. intros x y;destruct x, y; simpl; norm. - apply (ARgen_phiPOS_add ARth). - apply gen_phiZ1_pos_sub. - rewrite gen_phiZ1_pos_sub. apply (Radd_comm Rth). - rewrite (ARgen_phiPOS_add ARth); norm. Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom