テンプレート

以下を前提にする

Require Import Arith List Omega ZArith.
From mathcomp Require Import all_ssreflect.
Import ListNotations.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.