proposition: Lemma solve_correct n m p s s1 s2 : (s1, s2) = fst (iter2s n) -> m <= n -> nsreachable m s -> nsreachable (m - p) (fold_left (fun s a => m2f a s) (solve p s s1 s2) s).
proof: Proof. intro H; generalize m s; elim p; clear m p s; simpl; auto. intros m; rewrite Nat.sub_0_r; auto. intros p Hrec m; case m; clear m; simpl. - intros s _ HH; case HH; intros HH1 _; inversion_clear HH1. rewrite get_next_init with (1 := H). split; try apply nreach0; intros m1 Hm1; contradict Hm1; auto with arith. - intros m s H1 H2. assert (F1: m < n); auto with arith. generalize (get_next_correct _ _ _ _ _ H F1 H2); case get_next. + intros a Ha; rewrite fold_left_cons. apply Hrec; auto with arith. + intros HH; case HH. Qed.
imports: ZArith List