-apply le_minus_m.apply le_n.
-rewrite > mod_n_n.reflexivity.
-apply (trans_lt ? (S O)).apply (le_n (S O)).unfold lt.
-apply le_S_S.apply le_S_S.apply le_O_n.
+apply (le_S_S_to_le (S (S O)) (S (S m1)) ?).
+apply (minus_le_O_to_le (S (S (S O))) (S (S (S m1))) ?).
+apply (le_n O).
+rewrite < sym_plus. simplify. apply le_n.
+apply (eq_to_eqb_true (mod (S (S m1)) (S (S m1))) O ?).
+apply (mod_n_n (S (S m1)) ?).
+apply (H).