proposition: Lemma smallest_aux_plus m : P (S m) -> forall k acc acc', smallest_aux acc (k + S m) = smallest_aux acc' (S m).
proof: Proof. intro PSm. induction k; intros acc acc'; simpl. destruct (P_dec (S m)). refl. contr. erewrite IHk. refl. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)