proposition: Lemma lt_q_qbr : forall b q r : nat, 0 < r -> one < b -> q < q * b + r.
proof: Proof. simple induction q; [ auto with arith | intros ]. apply lt_trans with (S n * b). auto with arith. pattern (S n * b) at 1 in |- *; rewrite (plus_n_O (S n * b)); auto with arith. Qed.
imports: Arith Constants Le_lt_compl Mult_compl