-lemma eq_div_div_times : \forall x,y,z.O < z \to O < y \to x/y = (z*x)/(z*y).
-intros.rewrite > (div_mod x y) in \vdash (? ? ? %);
- [rewrite > distr_times_plus;rewrite > sym_times;rewrite > assoc_times;
- rewrite > sym_times in ⊢ (? ? ? (? (? (? ? %) ?) ?));
- rewrite > div_plus_times
- [reflexivity
- |generalize in match H;cases z;intros
- [elim (not_le_Sn_O ? H2)
- |apply lt_times_r;apply lt_mod_m_m;assumption]]
- |assumption]
-qed.
-