intros 4; cases X (x Hx); clear X; letin X ≝ ≪x,Hx≫;
fold normalize X; intros; cases H1;
alias symbol "N" = "Natural numbers".
intros 4; cases X (x Hx); clear X; letin X ≝ ≪x,Hx≫;
fold normalize X; intros; cases H1;
alias symbol "N" = "Natural numbers".
∀i:nat.∃j:nat.spec i j));[whd; apply nP;] unfold spec in aux ⊢ %;
[3: unfold X in H2; clear H4 n aux spec H3 H1 H X;
cases (cases_in_segment ??? Hx);
∀i:nat.∃j:nat.spec i j));[whd; apply nP;] unfold spec in aux ⊢ %;
[3: unfold X in H2; clear H4 n aux spec H3 H1 H X;
cases (cases_in_segment ??? Hx);
cases H5; clear H5; cases H7; clear H7;
[1: left; split; [ apply (le_S ?? H5); | assumption]
|3: cases (?:False); rewrite < H8 in H6; apply (not_le_Sn_n ? H6);
cases H5; clear H5; cases H7; clear H7;
[1: left; split; [ apply (le_S ?? H5); | assumption]
|3: cases (?:False); rewrite < H8 in H6; apply (not_le_Sn_n ? H6);
clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut;
cut (x = S (\fst (a w)));
[2: apply le_to_le_to_eq; [2: assumption]
clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut;
cut (x = S (\fst (a w)));
[2: apply le_to_le_to_eq; [2: assumption]
apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm;
apply (le_plus ???? (le_n ?) H9);]]]]
clearbody m; unfold spec in m; clear spec;
apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm;
apply (le_plus ???? (le_n ?) H9);]]]]
clearbody m; unfold spec in m; clear spec;
[1: cases (find (S n) n2); intro; change with (x = \fst (a w));
apply H6; rewrite < H7; simplify; apply plus_n_Sm;
|2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity
|3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1;
[1: cases (find (S n) n2); intro; change with (x = \fst (a w));
apply H6; rewrite < H7; simplify; apply plus_n_Sm;
|2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity
|3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1;