proposition: Lemma gen_Zeqb_ok : forall x y, Zeq_bool x y = true -> [x] == [y].
proof: Proof. intros x y H7. assert (H10 := Zeq_bool_eq x y H7);unfold IDphi in H10. rewrite H10;reflexivity. Qed.
imports: ZArith_base Zpow_def BinInt BinNat Setoid BinList BinPos BinNat BinInt Setoid Ncring Ncring_polynom