proposition: Lemma lt_O_q : forall b q r : nat, b < q * b + r -> 0 < r -> r < b -> 0 < q.
proof: Proof. intros; case (lt_or_Zero q); [ auto with arith | intros ]. absurd (b < r). apply lt_asym; auto with arith. replace r with (q * b + r); auto with arith. rewrite H2; simpl in |- *; auto with arith. Qed.
imports: Arith Constants Le_lt_compl Mult_compl