-generalize in match (refl_eq nat (m q));
-generalize in match (m q) in ⊢ (? ? ? % → %); intro X; cases X; clear X;
-intros; simplify in H12:(? ? ? %); simplify in ⊢ (? ? (? ? ? % ?));
-generalize in match (refl_eq nat (m r));
-generalize in match (m r) in ⊢ (? ? ? % → %); intro X; cases X; clear X;
-intros; simplify in H14:(? ? ? %); simplify in ⊢ (? ? (? ? ? ? %));
-generalize in match (refl_eq nat (m p));
-generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X; clear X;
-intros; simplify in H16:(? ? ? %);
-apply H15; [3: apply le_n] destruct H16; destruct H14; destruct H12; clear H11 H13 H15;
-[1: lapply (trans_increasing ?? Hm1 p q) as T; [apply not_lt_to_le; apply T;]
- apply (le_to_not_lt p q H5);
-|2: lapply (trans_increasing ?? Hm1 p r) as T; [apply not_lt_to_le; apply T;]
- apply (le_to_not_lt p r H10);]
-qed.
\ No newline at end of file
+generalize in match (refl_eq nat (m p));
+generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X;
+intros (H16); simplify in H16:(? ? ? %); destruct H16;
+apply H15; [3: apply le_n]
+[1: lapply (trans_increasing ? Hm1 p q) as T; [apply not_lt_to_le; apply T;]
+ apply (le_to_not_lt p q H4);
+|2: lapply (trans_increasing ? Hm1 p r) as T; [apply not_lt_to_le; apply T;]
+ apply (le_to_not_lt p r H5);]
+qed.