proposition: Lemma smallest_aux_ok : forall k acc, P acc -> P (smallest_aux acc k).
proof: Proof. induction k; intros acc Pacc; simpl. destruct (P_dec 0); hyp. destruct (P_dec (S k)); fo. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)