LATEX/2025bad-foundations-lean.tex (htmlized)

Warning: this is an htmlized version!
The original is here, and
the conversion rules are here.
% This file:
%   http://anggtwu.net/LATEX/2025bad-foundations-lean.tex.html
%   http://anggtwu.net/LATEX/2025bad-foundations-lean.tex
%          (find-angg "LATEX/2025bad-foundations-lean.tex")
% Author: Eduardo Ochs <eduardoochs@gmail.com>
%
% (defun e () (interactive) (find-angg "LATEX/2025bad-foundations-lean.tex"))
% (find-es "pygments")

\makeatletter
\def\PY@reset{\let\PY@it=\relax \let\PY@bf=\relax%
    \let\PY@ul=\relax \let\PY@tc=\relax%
    \let\PY@bc=\relax \let\PY@ff=\relax}
\def\PY@tok#1{\csname PY@tok@#1\endcsname}
\def\PY@toks#1+{\ifx\relax#1\empty\else%
    \PY@tok{#1}\expandafter\PY@toks\fi}
\def\PY@do#1{\PY@bc{\PY@tc{\PY@ul{%
    \PY@it{\PY@bf{\PY@ff{#1}}}}}}}
\def\PY#1#2{\PY@reset\PY@toks#1+\relax+\PY@do{#2}}

\@namedef{PY@tok@w}{\def\PY@tc##1{\textcolor[rgb]{0.73,0.73,0.73}{##1}}}
\@namedef{PY@tok@c}{\let\PY@it=\textit\def\PY@tc##1{\textcolor[rgb]{0.24,0.48,0.48}{##1}}}
\@namedef{PY@tok@cp}{\def\PY@tc##1{\textcolor[rgb]{0.61,0.40,0.00}{##1}}}
\@namedef{PY@tok@k}{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\@namedef{PY@tok@kp}{\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\@namedef{PY@tok@kt}{\def\PY@tc##1{\textcolor[rgb]{0.69,0.00,0.25}{##1}}}
\@namedef{PY@tok@o}{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
\@namedef{PY@tok@ow}{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.67,0.13,1.00}{##1}}}
\@namedef{PY@tok@nb}{\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\@namedef{PY@tok@nf}{\def\PY@tc##1{\textcolor[rgb]{0.00,0.00,1.00}{##1}}}
\@namedef{PY@tok@nc}{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.00,1.00}{##1}}}
\@namedef{PY@tok@nn}{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.00,1.00}{##1}}}
\@namedef{PY@tok@ne}{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.80,0.25,0.22}{##1}}}
\@namedef{PY@tok@nv}{\def\PY@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
\@namedef{PY@tok@no}{\def\PY@tc##1{\textcolor[rgb]{0.53,0.00,0.00}{##1}}}
\@namedef{PY@tok@nl}{\def\PY@tc##1{\textcolor[rgb]{0.46,0.46,0.00}{##1}}}
\@namedef{PY@tok@ni}{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.44,0.44,0.44}{##1}}}
\@namedef{PY@tok@na}{\def\PY@tc##1{\textcolor[rgb]{0.41,0.47,0.13}{##1}}}
\@namedef{PY@tok@nt}{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\@namedef{PY@tok@nd}{\def\PY@tc##1{\textcolor[rgb]{0.67,0.13,1.00}{##1}}}
\@namedef{PY@tok@s}{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
\@namedef{PY@tok@sd}{\let\PY@it=\textit\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
\@namedef{PY@tok@si}{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.64,0.35,0.47}{##1}}}
\@namedef{PY@tok@se}{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.67,0.36,0.12}{##1}}}
\@namedef{PY@tok@sr}{\def\PY@tc##1{\textcolor[rgb]{0.64,0.35,0.47}{##1}}}
\@namedef{PY@tok@ss}{\def\PY@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
\@namedef{PY@tok@sx}{\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\@namedef{PY@tok@m}{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
\@namedef{PY@tok@gh}{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.00,0.50}{##1}}}
\@namedef{PY@tok@gu}{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.50,0.00,0.50}{##1}}}
\@namedef{PY@tok@gd}{\def\PY@tc##1{\textcolor[rgb]{0.63,0.00,0.00}{##1}}}
\@namedef{PY@tok@gi}{\def\PY@tc##1{\textcolor[rgb]{0.00,0.52,0.00}{##1}}}
\@namedef{PY@tok@gr}{\def\PY@tc##1{\textcolor[rgb]{0.89,0.00,0.00}{##1}}}
\@namedef{PY@tok@ge}{\let\PY@it=\textit}
\@namedef{PY@tok@gs}{\let\PY@bf=\textbf}
\@namedef{PY@tok@ges}{\let\PY@bf=\textbf\let\PY@it=\textit}
\@namedef{PY@tok@gp}{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.00,0.50}{##1}}}
\@namedef{PY@tok@go}{\def\PY@tc##1{\textcolor[rgb]{0.44,0.44,0.44}{##1}}}
\@namedef{PY@tok@gt}{\def\PY@tc##1{\textcolor[rgb]{0.00,0.27,0.87}{##1}}}
\@namedef{PY@tok@err}{\def\PY@bc##1{{\setlength{\fboxsep}{\string -\fboxrule}\fcolorbox[rgb]{1.00,0.00,0.00}{1,1,1}{\strut ##1}}}}
\@namedef{PY@tok@kc}{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\@namedef{PY@tok@kd}{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\@namedef{PY@tok@kn}{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\@namedef{PY@tok@kr}{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\@namedef{PY@tok@bp}{\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\@namedef{PY@tok@fm}{\def\PY@tc##1{\textcolor[rgb]{0.00,0.00,1.00}{##1}}}
\@namedef{PY@tok@vc}{\def\PY@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
\@namedef{PY@tok@vg}{\def\PY@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
\@namedef{PY@tok@vi}{\def\PY@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
\@namedef{PY@tok@vm}{\def\PY@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
\@namedef{PY@tok@sa}{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
\@namedef{PY@tok@sb}{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
\@namedef{PY@tok@sc}{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
\@namedef{PY@tok@dl}{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
\@namedef{PY@tok@s2}{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
\@namedef{PY@tok@sh}{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
\@namedef{PY@tok@s1}{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
\@namedef{PY@tok@mb}{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
\@namedef{PY@tok@mf}{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
\@namedef{PY@tok@mh}{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
\@namedef{PY@tok@mi}{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
\@namedef{PY@tok@il}{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
\@namedef{PY@tok@mo}{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
\@namedef{PY@tok@ch}{\let\PY@it=\textit\def\PY@tc##1{\textcolor[rgb]{0.24,0.48,0.48}{##1}}}
\@namedef{PY@tok@cm}{\let\PY@it=\textit\def\PY@tc##1{\textcolor[rgb]{0.24,0.48,0.48}{##1}}}
\@namedef{PY@tok@cpf}{\let\PY@it=\textit\def\PY@tc##1{\textcolor[rgb]{0.24,0.48,0.48}{##1}}}
\@namedef{PY@tok@c1}{\let\PY@it=\textit\def\PY@tc##1{\textcolor[rgb]{0.24,0.48,0.48}{##1}}}
\@namedef{PY@tok@cs}{\let\PY@it=\textit\def\PY@tc##1{\textcolor[rgb]{0.24,0.48,0.48}{##1}}}

\def\PYZbs{\char`\\}
\def\PYZus{\char`\_}
\def\PYZob{\char`\{}
\def\PYZcb{\char`\}}
\def\PYZca{\char`\^}
\def\PYZam{\char`\&}
\def\PYZlt{\char`\<}
\def\PYZgt{\char`\>}
\def\PYZsh{\char`\#}
\def\PYZpc{\char`\%}
\def\PYZdl{\char`\$}
\def\PYZhy{\char`\-}
\def\PYZsq{\char`\'}
\def\PYZdq{\char`\"}
\def\PYZti{\char`\~}
% for compatibility with earlier versions
\def\PYZat{@}
\def\PYZlb{[}
\def\PYZrb{]}
\makeatother

%V \PY{k+kn}{variable}\PY{+w}{ }\PY{o}{(}\PY{n}{a}\PY{+w}{ }\PY{n}{b}\PY{+w}{ }\PY{n}{c}\PY{+w}{ }\PY{n}{d}\PY{+w}{ }\PY{n}{e}\PY{+w}{ }\PY{o}{:}\PY{+w}{ }\PY{n}{Nat}\PY{o}{)}
%V \PY{k+kn}{variable}\PY{+w}{ }\PY{o}{(}\PY{n}{h1}\PY{+w}{ }\PY{o}{:}\PY{+w}{ }\PY{n}{a}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{n}{b}\PY{o}{)}
%V \PY{k+kn}{variable}\PY{+w}{ }\PY{o}{(}\PY{n}{h2}\PY{+w}{ }\PY{o}{:}\PY{+w}{ }\PY{n}{b}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{n}{c}\PY{+w}{ }\PY{n+nb+bp}{+}\PY{+w}{ }\PY{l+m+mi}{1}\PY{o}{)}
%V \PY{k+kn}{variable}\PY{+w}{ }\PY{o}{(}\PY{n}{h3}\PY{+w}{ }\PY{o}{:}\PY{+w}{ }\PY{n}{c}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{n}{d}\PY{o}{)}
%V \PY{k+kn}{variable}\PY{+w}{ }\PY{o}{(}\PY{n}{h4}\PY{+w}{ }\PY{o}{:}\PY{+w}{ }\PY{n}{e}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{l+m+mi}{1}\PY{+w}{ }\PY{n+nb+bp}{+}\PY{+w}{ }\PY{n}{d}\PY{o}{)}
%V 
%V \PY{n}{include}\PY{+w}{ }\PY{n}{h1}\PY{+w}{ }\PY{n}{h2}\PY{+w}{ }\PY{n}{h3}\PY{+w}{ }\PY{n}{h4}\PY{+w}{ }\PY{k}{in}
%V \PY{k+kn}{theorem}\PY{+w}{ }\PY{n}{T1}\PY{+w}{ }\PY{o}{:}\PY{+w}{ }\PY{n}{a}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{n}{e}\PY{+w}{ }\PY{o}{:=}
%V \PY{+w}{  }\PY{k}{by}\PY{+w}{ }\PY{n}{rw}\PY{+w}{ }\PY{o}{[}\PY{n}{h1}\PY{o}{,}\PY{+w}{ }\PY{n}{h2}\PY{o}{,}\PY{+w}{ }\PY{n}{h3}\PY{o}{,}\PY{+w}{ }\PY{n}{Nat}\PY{n+nb+bp}{.}\PY{n}{add\PYZus{}comm}\PY{o}{,}\PY{+w}{ }\PY{n}{h4}\PY{o}{]}
%V 
%V \PY{n}{include}\PY{+w}{ }\PY{n}{h1}\PY{+w}{ }\PY{n}{h2}\PY{+w}{ }\PY{n}{h3}\PY{+w}{ }\PY{n}{h4}\PY{+w}{ }\PY{k}{in}
%V \PY{k+kn}{theorem}\PY{+w}{ }\PY{n}{T2}\PY{+w}{ }\PY{o}{:}
%V \PY{+w}{  }\PY{n}{a}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{n}{e}\PY{+w}{     }\PY{o}{:=}\PY{+w}{ }\PY{k}{calc}
%V \PY{+w}{  }\PY{n}{a}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{n}{d}\PY{+w}{ }\PY{n+nb+bp}{+}\PY{+w}{ }\PY{l+m+mi}{1}\PY{+w}{ }\PY{o}{:=}\PY{+w}{ }\PY{k}{by}\PY{+w}{ }\PY{n}{rw}\PY{+w}{ }\PY{o}{[}\PY{n}{h1}\PY{o}{,}\PY{+w}{ }\PY{n}{h2}\PY{o}{,}\PY{+w}{ }\PY{n}{h3}\PY{o}{]}
%V \PY{+w}{  }\PY{n+nb+bp}{\PYZus{}}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{l+m+mi}{1}\PY{+w}{ }\PY{n+nb+bp}{+}\PY{+w}{ }\PY{n}{d}\PY{+w}{ }\PY{o}{:=}\PY{+w}{ }\PY{k}{by}\PY{+w}{ }\PY{n}{rw}\PY{+w}{ }\PY{o}{[}\PY{n}{Nat}\PY{n+nb+bp}{.}\PY{n}{add\PYZus{}comm}\PY{o}{]}
%V \PY{+w}{  }\PY{n+nb+bp}{\PYZus{}}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{n}{e}\PY{+w}{     }\PY{o}{:=}\PY{+w}{ }\PY{k}{by}\PY{+w}{ }\PY{n}{rw}\PY{+w}{ }\PY{o}{[}\PY{n}{h4}\PY{o}{]}
%V 
%V \PY{n}{include}\PY{+w}{ }\PY{n}{h1}\PY{+w}{ }\PY{n}{h2}\PY{+w}{ }\PY{n}{h3}\PY{+w}{ }\PY{n}{h4}\PY{+w}{ }\PY{k}{in}
%V \PY{k+kn}{theorem}\PY{+w}{ }\PY{n}{T3}\PY{+w}{ }\PY{o}{:}
%V \PY{+w}{  }\PY{n}{a}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{n}{e}\PY{+w}{     }\PY{o}{:=}\PY{+w}{ }\PY{k}{calc}
%V \PY{+w}{  }\PY{n}{a}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{n}{b}\PY{+w}{     }\PY{o}{:=}\PY{+w}{ }\PY{k}{by}\PY{+w}{ }\PY{n}{rw}\PY{+w}{ }\PY{o}{[}\PY{n}{h1}\PY{o}{]}
%V \PY{+w}{  }\PY{n+nb+bp}{\PYZus{}}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{n}{c}\PY{+w}{ }\PY{n+nb+bp}{+}\PY{+w}{ }\PY{l+m+mi}{1}\PY{+w}{ }\PY{o}{:=}\PY{+w}{ }\PY{k}{by}\PY{+w}{ }\PY{n}{rw}\PY{+w}{ }\PY{o}{[}\PY{n}{h2}\PY{o}{]}
%V \PY{+w}{  }\PY{n+nb+bp}{\PYZus{}}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{n}{d}\PY{+w}{ }\PY{n+nb+bp}{+}\PY{+w}{ }\PY{l+m+mi}{1}\PY{+w}{ }\PY{o}{:=}\PY{+w}{ }\PY{k}{by}\PY{+w}{ }\PY{n}{rw}\PY{+w}{ }\PY{o}{[}\PY{n}{h3}\PY{o}{]}
%V \PY{+w}{  }\PY{n+nb+bp}{\PYZus{}}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{l+m+mi}{1}\PY{+w}{ }\PY{n+nb+bp}{+}\PY{+w}{ }\PY{n}{d}\PY{+w}{ }\PY{o}{:=}\PY{+w}{ }\PY{k}{by}\PY{+w}{ }\PY{n}{rw}\PY{+w}{ }\PY{o}{[}\PY{n}{Nat}\PY{n+nb+bp}{.}\PY{n}{add\PYZus{}comm}\PY{o}{]}
%V \PY{+w}{  }\PY{n+nb+bp}{\PYZus{}}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{n}{e}\PY{+w}{     }\PY{o}{:=}\PY{+w}{ }\PY{k}{by}\PY{+w}{ }\PY{n}{rw}\PY{+w}{ }\PY{o}{[}\PY{n}{h4}\PY{o}{]}
%V 
%V \PY{n}{include}\PY{+w}{ }\PY{n}{h1}\PY{+w}{ }\PY{n}{h2}\PY{+w}{ }\PY{n}{h3}\PY{+w}{ }\PY{n}{h4}\PY{+w}{ }\PY{k}{in}
%V \PY{k+kn}{theorem}\PY{+w}{ }\PY{n}{T4}\PY{+w}{ }\PY{o}{:}
%V \PY{+w}{  }\PY{n}{a}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{n}{e}\PY{+w}{     }\PY{o}{:=}\PY{+w}{ }\PY{k}{calc}
%V \PY{+w}{  }\PY{n}{a}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{n}{b}\PY{+w}{     }\PY{o}{:=}\PY{+w}{ }\PY{n}{h1}
%V \PY{+w}{  }\PY{n+nb+bp}{\PYZus{}}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{n}{c}\PY{+w}{ }\PY{n+nb+bp}{+}\PY{+w}{ }\PY{l+m+mi}{1}\PY{+w}{ }\PY{o}{:=}\PY{+w}{ }\PY{n}{h2}
%V \PY{+w}{  }\PY{n+nb+bp}{\PYZus{}}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{n}{d}\PY{+w}{ }\PY{n+nb+bp}{+}\PY{+w}{ }\PY{l+m+mi}{1}\PY{+w}{ }\PY{o}{:=}\PY{+w}{ }\PY{n}{congrArg}\PY{+w}{ }\PY{n}{Nat}\PY{n+nb+bp}{.}\PY{n}{succ}\PY{+w}{ }\PY{n}{h3}
%V \PY{+w}{  }\PY{n+nb+bp}{\PYZus{}}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{l+m+mi}{1}\PY{+w}{ }\PY{n+nb+bp}{+}\PY{+w}{ }\PY{n}{d}\PY{+w}{ }\PY{o}{:=}\PY{+w}{ }\PY{n}{Nat}\PY{n+nb+bp}{.}\PY{n}{add\PYZus{}comm}\PY{+w}{ }\PY{n}{d}\PY{+w}{ }\PY{l+m+mi}{1}
%V \PY{+w}{  }\PY{n+nb+bp}{\PYZus{}}\PY{+w}{ }\PY{n+nb+bp}{=}\PY{+w}{ }\PY{n}{e}\PY{+w}{     }\PY{o}{:=}\PY{+w}{ }\PY{n}{Eq}\PY{n+nb+bp}{.}\PY{n}{symm}\PY{+w}{ }\PY{n}{h4}



% Local Variables:
% coding:  utf-8-unix
% End: