apply le_plus_n_r;]
|2,3: clear H6;
cases (aux n1) in H5 ⊢ %; intros;
- change in match (a â\8c©w,H5â\8cª) in H6 ⊢ % with (a w);
+ change in match (a â\89ªw,H5â\89«) in H6 ⊢ % with (a w);
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);