proposition: Lemma gen_phiZ1_pos_sub : forall x y, gen_phiZ1 (Z.pos_sub x y) == gen_phiPOS1 x + -gen_phiPOS1 y.
proof: Proof. intros x y. rewrite Z.pos_sub_spec. case Pos.compare_spec; intros H; simpl. - rewrite H. rewrite (Ropp_def Rth);rrefl. - rewrite <- (Pos.sub_add y x H) at 2. rewrite Pos.add_comm. rewrite (ARgen_phiPOS_add ARth);simpl;norm. rewrite (Ropp_def Rth);norm. - rewrite <- (Pos.sub_add x y H) at 2. rewrite (ARgen_phiPOS_add ARth);simpl;norm. add_push (gen_phiPOS1 (x-y));rewrite (Ropp_def Rth); norm. Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom