proposition: Lemma quotient_positive : forall q n n0 : nat, n = q * n0 -> 0 < n -> 0 < q.
proof: Proof. intros q n n0 H H0. case (lt_or_Zero q); [ auto with arith | intro H1 ]. absurd (0 < q * n0). rewrite H1; simpl in |- *; auto with arith. rewrite <- H; auto with arith. Qed.
imports: Arith Constants Le_lt_compl