Solution.v

Require Import Problem Eqdep_dec.

(* HINT *)
Scheme le_max_ind := Induction for le Sort Prop.

(* HINT 2: Eqdep_dec.UIP_refl_nat *)

(* BEWARE: do not use Program.Equality, which imports extra axioms from JMeq *)

Theorem solution: task.
Proof.
  unfold task.
Admitted.