From mathcomp Require Import all_ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. (** ---------------------------------------------------------- #
# ** title body - item [verbatim code] - item # $$ \frac{1}{2} $$ # #
# *) Check nat. (** #
# #
(notes)
# footnote #a link# end footnote #
# #
# *)