proposition: Lemma fpeq_wd : forall a b:Z, a=b -> (zfp a)[=](zfp b).
proof: Proof. intros a b heq. simpl. unfold zfp in *. unfold ZModeq in *. elim heq. auto with *. Qed.
imports: CoRN.model.Zmod.Zm CoRN.model.rings.Zring CoRN.algebra.CPoly_Degree