intros; lapply (H5 i j) as H14;
[2: apply (max_le_l ??? H6);|3:apply (max_le_l ??? H7);]
cases (le_to_or_lt_eq ?? H10); [2: destruct H11; destruct H4; assumption]
- generalize in match H6; generalize in match H7;
- cases (aux n1); simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
- apply H12; [3: apply le_S_S_to_le; assumption]
+ cases (aux n1) in H6 H7 ⊢ %; simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
+ apply H6; [3: apply le_S_S_to_le; assumption]
apply lt_to_le; apply (max_le_r w1); assumption;
|4: intros; clear H6; rewrite > H4 in H5;
rewrite < (le_n_O_to_eq ? H11); apply H5; assumption;]