include "arithmetics/pidgeon_hole.ma".
include "basics/sets.ma".
include "basics/types.ma".
+include "basics/core_notation/card_1.ma".
(************************************ MAX *************************************)
notation "Max_{ ident i < n | p } f"
|%{1} %{0} #n #_ >commutative_times <times_n_1
@monotonic_sU // >size_f_size >size_of_size //
]
-qed.
\ No newline at end of file
+qed.