proposition: Theorem NPEsub_ok e1 e2: (e1 -- e2 === e1 - e2)%poly.
proof: Proof. intros l. destruct e1, e2; simpl; try reflexivity; try case ceqb_spec; try intro H; try rewrite H; simpl; try rewrite phi_0; try reflexivity; try (symmetry; apply rsub_0_l); try (symmetry; apply rsub_0_r). apply (morph_sub CRmorph). Qed.
imports: ZArith_base