proposition: Lemma triv_div_th : Ring_theory.div_theory req cadd cmul phi triv_div.
proof: Proof. constructor. intros a b;unfold triv_div. assert (X:= morph_eq morph a b);destruct (ceqb a b). - Esimpl. rewrite X; trivial. rsimpl. - Esimpl; rsimpl. Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom