elim (p_ord_aux n (n1 / m) m).
apply H5.assumption.
apply eq_mod_O_to_lt_O_div.
-apply (trans_lt ? (S O)).simplify.apply le_n.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.
assumption.assumption.assumption.
apply le_S_S_to_le.
apply (trans_le ? n1).change with (n1 / m < n1).
intros.
change with (n1 \mod m \neq O).
rewrite > H4.
-(* Andrea: META NOT FOUND !!!
-rewrite > sym_eq. *)
-simplify.intro.
+unfold Not.intro.
apply (not_eq_O_S m1).
rewrite > H5.reflexivity.
qed.