proposition: Lemma solve_init n s s1 s2 : (s1, s2) = fst (iter2s n) -> nlreachable n s -> fold_left (fun s a => m2f a s) (solve n s s1 s2) s = init_state.
proof: Proof. intros H1 H2. case (nlreachable_bound _ _ H2); clear H2; intros m (H2, H3). generalize (solve_correct n m n s s1 s2 H1 H2 H3). replace (m - n) with 0. - intros (HH,_); inversion HH; auto. - apply Nat.lt_eq_cases in H2; destruct H2; subst; auto with arith. apply Nat.lt_le_incl in H. apply Nat.sub_0_le in H; auto with arith. Qed.
imports: ZArith List