include "arithmetics/pidgeon_hole.ma".
include "basics/sets.ma".
include "basics/types.ma".
include "arithmetics/pidgeon_hole.ma".
include "basics/sets.ma".
include "basics/types.ma".
(************************************ MAX *************************************)
notation "Max_{ ident i < n | p } f"
(************************************ MAX *************************************)
notation "Max_{ ident i < n | p } f"