proposition: Lemma Ntriv_div_th : div_theory req N.add N.mul nphi N.div_eucl.
proof: Proof. constructor. intros a b; generalize (N.div_eucl_spec a b); case N.div_eucl; intros; subst. rewrite N.mul_comm; rsimpl. Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom