proposition: Lemma cring_div_theory: div_theory _==_ Z.add Z.mul Ncring_initial.gen_phiZ Z.quotrem.
proof: Proof. intros. apply InitialRing.Ztriv_div_th. unfold Setoid_Theory. simpl. apply ring_setoid. Defined.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool ZArith_base Algebra_syntax Ncring Ncring_initial Ncring_tac InitialRing