proposition: Lemma quotient_gt_one : forall q n n0 : nat, n0 < n -> n = q * n0 -> one < q.
proof: Proof. intros q n n0 H H0; case (one_cases q); [ auto with arith | simple induction 1; intro; absurd (n0 < n); auto with arith ]. rewrite H0; rewrite H2; auto with arith. rewrite H0; rewrite H2; simpl in |- *; rewrite <- plus_n_O; auto with arith. Qed.
imports: Arith Constants Le_lt_compl