elim Hcut.rewrite > divides_to_divides_b_true.
simplify.
split.assumption.apply witness n1 n1 (S O).apply times_n_SO.
elim Hcut.rewrite > divides_to_divides_b_true.
simplify.
split.assumption.apply witness n1 n1 (S O).apply times_n_SO.
apply le_to_or_lt_eq.apply le_O_n.
apply lt_to_le.
apply lt_mod_m_m.assumption.
apply le_S_S_to_le.
apply trans_le ? n1.
change with mod m n1 < n1.
apply le_to_or_lt_eq.apply le_O_n.
apply lt_to_le.
apply lt_mod_m_m.assumption.
apply le_S_S_to_le.
apply trans_le ? n1.
change with mod m n1 < n1.
elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption.
apply gcd_O_to_eq_O.apply sym_eq.assumption.
apply le_to_or_lt_eq.apply le_O_n.
elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption.
apply gcd_O_to_eq_O.apply sym_eq.assumption.
apply le_to_or_lt_eq.apply le_O_n.
apply decidable_divides n p.
apply trans_lt ? (S O).simplify.apply le_n.
simplify in H.elim H. assumption.
apply decidable_divides n p.
apply trans_lt ? (S O).simplify.apply le_n.
simplify in H.elim H. assumption.