proposition: Lemma get_next_aux_correct n s s1 s2 l : match get_next_aux n s s1 s2 l with Some a => In a l /\ get_number (m2f a s) s1 s2 = n | None => forall a, In a l -> get_number (m2f a s) s1 s2 <> n end.
proof: Proof. elim l; simpl; auto. intros a l1 Hrec; generalize (positive_eq_correct n (get_number (m2f a s) s1 s2)); case positive_eq; try (intros; discriminate); auto. generalize Hrec; case get_next_aux; auto. - intros m1 (H1, H2) H3; auto. - intros H1 H2 a1 [H3 | H3]; subst; auto. Qed.
imports: ZArith List