proposition: Theorem lap_mul_comm : ∀ a b, lap_eq (lap_mul a b) (lap_mul b a).
proof: Proof. intros a b. unfold lap_mul. rewrite lap_convol_mul_comm, Nat.add_comm; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation