proposition: Theorem poly_mul_comm : ∀ a b, (a * b = b * a)%pol.
proof: Proof. intros a b. unfold eq_poly; simpl. unfold lap_mul; simpl. rewrite Nat.add_comm. rewrite lap_convol_mul_comm; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation