apply le_times_l.
assumption.
apply le_times_r.assumption.
-alias id "not_eq_to_le_to_lt" = "cic:/matita/algebra/finite_groups/not_eq_to_le_to_lt.con".
-apply not_eq_to_le_to_lt.
+ apply not_eq_to_le_to_lt.
unfold.intro.apply H1.
rewrite < H3.
apply (witness ? r r ?).simplify.apply plus_n_O.
intros.rewrite > eq_p_ord_inv.
apply mod_plus_times.
assumption.
-qed.
\ No newline at end of file
+qed.