proposition: Lemma smallest_aux_le_exists k l acc : k <= l -> exists acc', smallest_aux acc l = smallest_aux acc' k.
proof: Proof. intro kl. destruct (le_plus kl) as [m e]; subst. apply smallest_aux_plus_exists. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)