fact: Definition at_most_one_pigeon_per_hole (dis:bool) (b:nat) (k:nat) := let F i j := if dis then (not (Pigeon_In_Hole i k) \/ not (Pigeon_In_Hole j k)) else (Pigeon_In_Hole i k -> Pigeon_In_Hole j k -> False) in Some (forall_2 (fun i j => if Nat.ltb i j then Some (F i j) else None) b b).
imports: List