proposition: Lemma lt_b_qbr : forall b q r : nat, 0 < r -> 0 < q -> r < b -> b < q * b + r.
proof: Proof. intros. apply le_lt_trans with (q * b). auto with arith. pattern (q * b) at 1 in |- *; rewrite plus_n_O; auto with arith. Qed.
imports: Arith Constants Le_lt_compl Mult_compl