proposition: Lemma smallest_aux_le k l acc acc' : k <= l -> P (S k) -> smallest_aux acc (S l) = smallest_aux acc' (S k).
proof: Proof. intros kl Pk. destruct (le_plus kl) as [m e]; subst. assert (e : S (m + k) = m + S k). lia. rewrite e. apply smallest_aux_plus. hyp. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)