proposition: Lemma smallest_inv_le k l : k <= l -> P k -> smallest l = smallest k.
proof: Proof. unfold smallest. destruct k; simpl. intros _ P0. destruct (P_dec 0). 2: contr. clear p. revert l. cut (forall l acc, smallest_aux acc l = 0). fo. induction l; intro acc; simpl. destruct (P_dec 0). refl. contr. fo. destruct l; simpl. lia. intro kl. apply smallest_aux_le. lia. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)