Library parking

Require Import ssreflect ssrfun ssrbool eqtype seq fintype ssrnat ssralg zmodp bigop.

Import GRing.Theory.

Section Parking.

(* Une grille est une fonction qui prend deux nombres et retourne un booléen  *)

Definition grid n := 'I_n -> 'I_n -> bool.

(* La somme sur une ligne                                                     *)

Definition sumL n (g : grid n) i := \sum_(j < n) g i j.

(* La somme sur une colonne                                                   *)

Definition sumC n (g : grid n) j := \sum_(i < n) g i j.

(* Deux petites propriétés pour pouvoir utiliser des arguments d'injectivité  *)

Lemma leq_sumL n (g : grid n) i : sumL g i < n.+1.

Lemma leq_sumC n (g : grid n) j : sumC g j < n.+1.

(* Dans une grille non vide, deux lignes ou deux colonnes, ou une ligne et une
   colonne ont la même somme                                                  *)

Lemma inl_inj {A B} : injective (@inl A B).
Lemma inr_inj {A B} : injective (@inr A B).

Lemma result n (g : grid n) : 0 < n ->
  exists i, exists j,
   [\/ (i != j) /\ (sumL g i = sumL g j),
        (i != j) /\ (sumC g i = sumC g j) | sumL g i = sumC g j].

End Parking.