proposition: Theorem NPEmul_ok e1 e2 : (e1 ** e2 === e1 * e2)%poly.
proof: Proof. intros l. revert e2; induction e1 as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1|? IHe1 n]; intro e2; destruct e2; simpl;try reflexivity; repeat (case ceqb_spec; intro H; try rewrite H; clear H); simpl; try reflexivity; try ring [phi_0 phi_1]. - apply (morph_mul CRmorph). - case N.eqb_spec; [intros <- | reflexivity]. rewrite NPEpow_ok. simpl. rewrite !rpow_pow. rewrite IHe1. destruct n; simpl; [ ring | apply pow_pos_mul_l ]. Qed.
imports: ZArith_base