proposition: Lemma repeated_rev n x: rev (repeat x n) = repeat x n.
proof: Proof. induction n; cbn; eauto. rewrite IHn. change [x] with (repeat x 1). rewrite <-repeated_plus. rewrite Nat.add_comm. reflexivity. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)