amintimany

From stdpp Require Import list.
From iris.algebra Require Import excl numbers gmap.
From iris.base_logic Require Export invariants saved_prop.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.

(* move *)
Lemma list_sum_replicate n m : list_sum (replicate n m) = n * m.
Proof.
  revert m; induction n as [|n IHn]; first done; intros ?; rewrite /= IHn; lia.