proposition: Lemma get_number_correct n n1 s s1 s2 : (s1, s2) = fst (iter2s n) -> n1 <= n -> nsreachable n1 s -> porder n1 = get_number s s1 s2.
proof: Proof. generalize (iter2s_correct n); case iter2s. intros (s3, s4) ss; simpl; intros (H1, (H2, H3)) HH Hl Hr. injection HH; intros; subst s3 s4; clear HH. unfold get_number. generalize (in_states_correct s s1); case in_states. - rewrite H1; intros (m, (Hm, (Hm1, Hm2))). assert(m = n1); subst. apply nsreachable_unique with s; auto. generalize (in_states_correct s s2); case in_states. + rewrite H2; intros (m1, (Hm3, (Hm4, Hm5))). assert (m1 = n1); subst. apply nsreachable_unique with s; auto. generalize Hm2 Hm5; generalize (porder_inv n1); intros [HH | [HH | HH]]; rewrite HH; auto. * intros _ HH1; case HH1; auto. * intros HH1; case HH1. + intros HH; generalize (positive_eq_correct (porder n1) 1); case positive_eq; auto; intros HH1. case HH; rewrite H2; exists n1; auto. - generalize (in_states_correct s s2); case in_states. + intros _ HH; generalize (porder_inv n1); intros [HH1 | [HH1 | HH1]]; rewrite HH1; auto. * case HH; rewrite H1; exists n1; rewrite HH1; simpl; auto. * case HH; rewrite H1; exists n1; rewrite HH1; simpl; auto. + intros HH HH1; generalize (porder_inv1 n1); intros [HH2 | HH2]. * case HH; rewrite H2; exists n1; auto. * case HH1; rewrite H1; exists n1; auto. Qed.
imports: ZArith List