proposition: Lemma gen_Zeqb_ok : forall x y, Zeq_bool x y = true -> [x] == [y].
proof: Proof. intros x y H. assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1. rewrite H1;rrefl. Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom