proposition: Lemma Zeqb_ok: forall x y : Z, Zeq_bool x y = true -> x == y.
proof: Proof. intros x y H. rewrite (Zeq_bool_eq x y H). reflexivity. Qed.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool ZArith Algebra_syntax Ncring Ncring_polynom Ncring_initial