proposition: Lemma smallest_aux_plus_exists m : forall k acc, exists acc', smallest_aux acc (k + m) = smallest_aux acc' m.
proof: Proof. induction k; intro acc; simpl. ex acc. refl. set (a := if P_dec (S (k + m)) then S (k + m) else acc). destruct (IHk a) as [acc' hacc']. ex acc'. hyp. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)