pi8027

From mathcomp Require Import ssreflect fintype finset seq ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(******************************************************************************

Coq/SSReflect formalization of the proof of 'f# ↘ (f∪g)# = f# ＼ (f∪g)#'.

Checked with Coq 8.8.0 and MathComp 1.7.0.

pi8027

\def\lst@Init#1{%
    \begingroup
    \ifx\lst@float\relax\else
        \edef\@tempa{\noexpand\lst@beginfloat{lstlisting}[\lst@float]}%
        \expandafter\@tempa
    \fi
    \ifx\lst@multicols\@empty\else
        \edef\lst@next{\noexpand\multicols{\lst@multicols}}
        \expandafter\lst@next
    \fi