-theorem bTIMESc_le_a_to_c_le_aDIVb: \forall a,b,c:nat.
-O \lt b \to (b*c) \le a \to c \le (a /b).
-intros.
-rewrite > (div_mod a b) in H1
-[ apply (le_times_to_le b ? ?)
- [ assumption
- | cut ( (c*b) \le ((a/b)*b) \lor ((a/b)*b) \lt (c*b))
- [ elim Hcut
- [ rewrite < (sym_times c b).
- rewrite < (sym_times (a/b) b).
- assumption
- | cut (a/b \lt c)
- [ change in Hcut1 with ((S (a/b)) \le c).
- cut( b*(S (a/b)) \le b*c)
- [ rewrite > (sym_times b (S (a/b))) in Hcut2.
- simplify in Hcut2.
- cut ((b + (a/b)*b) \le ((a/b)*b + (a \mod b)))
- [ cut (b \le (a \mod b))
- [ apply False_ind.
- apply (lt_to_not_le (a \mod b) b)
- [ apply (lt_mod_m_m).
- assumption
- | assumption
- ]
- | apply (le_plus_to_le ((a/b)*b)).
- rewrite > sym_plus.
- assumption.
- ]
- | apply (trans_le ? (b*c) ?);
- assumption
- ]
- | apply (le_times_r b ? ?).
- assumption
- ]
- | apply (lt_times_n_to_lt b (a/b) c)
- [ assumption
- | assumption
- ]
- ]
- ]
- | apply (leb_elim (c*b) ((a/b)*b))
- [ intros.
- left.
- assumption
- | intros.
- right.
- apply cic:/matita/nat/orders/not_le_to_lt.con.
- assumption
- ]
- ]
- ]
-| assumption
-]
-qed.
-