theorem le_mod_aux_m_m:
\forall p,n,m. n \leq p \to (mod_aux p n m) \leq m.
intro.
elim p
[ apply (le_n_O_elim n H (\lambda n.(mod_aux O n m) \leq m)).
theorem le_mod_aux_m_m:
\forall p,n,m. n \leq p \to (mod_aux p n m) \leq m.
intro.
elim p
[ apply (le_n_O_elim n H (\lambda n.(mod_aux O n m) \leq m)).
theorem div_mod_spec_div_mod:
\forall n,m. O < m \to (div_mod_spec n m (n / m) (n \mod m)).
intros.
theorem div_mod_spec_div_mod:
\forall n,m. O < m \to (div_mod_spec n m (n / m) (n \mod m)).
intros.
theorem div_times: \forall n,m:nat. ((S n)*m) / (S n) = m.
intros.
apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O);
theorem div_times: \forall n,m:nat. ((S n)*m) / (S n) = m.
intros.
apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O);
((S n) \mod m) = S (n \mod m).
intros.
apply (div_mod_spec_to_eq2 (S n) m ((S n) / m) ((S n) \mod m) (n / m) (S (n \mod m)))
((S n) \mod m) = S (n \mod m).
intros.
apply (div_mod_spec_to_eq2 (S n) m ((S n) / m) ((S n) \mod m) (n / m) (S (n \mod m)))