千衣アンテナ＠はてな

すべて | グループ指定なし | 定期チェック | NSFW | その他 | tom

おとなりアンテナ | おすすめページ

1. 2025/03/22 12:45:27 天泣記

   2025-03-20 (Thu)
   #1 あみだくじ (2)
   証明の場合分けが不必要に多かったので減らしてみた。
   (他にもいくらか調整した。)
   From mathcomp Require Import all_ssreflect.
   Section amida_kuji.
   Variable segment : eqType.
   Definition path := seq segment.
   (* ami