proposition: Lemma smallest_aux_le_max_args l : forall k acc, acc <= l -> k <= l -> smallest_aux acc k <= l.
proof: Proof. induction k; intros acc accl kl; simpl. destruct (P_dec 0); lia. destruct (P_dec (S k)); apply IHk; lia. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)