proposition: Theorem lap_mul_1_r : ∀ la, lap_eq (lap_mul la [1%K]) la.
proof: Proof. intros la. unfold lap_mul. apply lap_convol_mul_1_r; simpl. rewrite Nat.add_comm; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation