%
\begin{isabellebody}%
\setisabellecontext{MoreBinomial}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ MoreBinomial\isanewline
\isakeyword{imports}\ Binomial\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
\isacommand{lemma}\isamarkupfalse%
\ choose{\isacharunderscore}mono{\isacharunderscore}Suc{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}Suc\ n\ choose\ k\ {\isasymge}\ n\ choose\ k{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ binomial{\isacharunderscore}Suc{\isacharunderscore}Suc{\isacharbrackleft}of\ n\ {\isachardoublequoteopen}k{\isacharminus}{\isadigit{1}}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}k{\isacharequal}{\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ choose{\isacharunderscore}mono{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}m\ {\isasymge}\ n{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}m\ choose\ k\ {\isasymge}\ n\ choose\ k{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ {\isachardoublequoteopen}m{\isacharminus}n{\isachardoublequoteclose}\ arbitrary{\isacharcolon}\ m\ n{\isacharparenright}\ \isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isadigit{0}}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Suc\ r{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ Suc{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ m\ {\isachardoublequoteopen}Suc\ n{\isachardoublequoteclose}{\isacharbrackright}\ Suc{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ Suc{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ choose{\isacharunderscore}mono{\isacharunderscore}Suc{\isacharbrackleft}of\ n\ k{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ n{\isacharunderscore}subsets{\isacharunderscore}ub{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymUnion}F\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}card\ {\isacharbraceleft}A\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isacharequal}\ k{\isacharbraceright}\ {\isasymle}\ n\ choose\ k{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharbraceleft}A\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isacharequal}\ k{\isacharbraceright}\ {\isasymsubseteq}\ {\isacharbraceleft}B{\isachardot}\ B\ {\isasymsubseteq}\ {\isasymUnion}F\ {\isasymand}\ card\ B\ {\isacharequal}\ k{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharbraceleft}A\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isacharequal}\ k{\isacharbraceright}\ {\isasymle}\ card\ {\isacharbraceleft}B{\isachardot}\ B\ {\isasymsubseteq}\ {\isasymUnion}F\ {\isasymand}\ card\ B\ {\isacharequal}\ k{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}mono{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharbraceleft}B{\isachardot}\ B\ {\isasymsubseteq}\ {\isasymUnion}F\ {\isasymand}\ card\ B\ {\isacharequal}\ k{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbraceleft}A\ {\isasymin}\ F{\isachardot}\ card\ A\ {\isacharequal}\ k{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\ assms\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\ \isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharparenleft}{\isasymUnion}F{\isacharparenright}\ choose\ k\ {\isasymle}\ n\ choose\ k{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ choose{\isacharunderscore}mono\ card{\isacharunderscore}mono{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ n{\isacharunderscore}subsets{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}\ k{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
