proposition: Theorem div_not_divides_S : forall p q : nat, 0 < q -> ~ divides q (S p) -> div (S p) q = div p q.
proof: Proof. intros p q H H1; apply sym_equal; apply div_unique; auto. apply Nat.le_trans with p; auto with arith. apply div_le; auto with arith. generalize (pdiv_def p q H); unfold div in |- *; case (pdiv p q); simpl in |- *. intros q1 r1 (H2, H3). rewrite H2. rewrite plus_n_Sm; auto. rewrite <- mult_n_Sm; auto. repeat rewrite (Nat.mul_comm q); auto with arith. apply Nat.add_lt_mono_l; auto with arith. case (proj1 (Nat.lt_eq_cases (S r1) q)); auto. intros H4; case H1; exists (S q1). rewrite H2. rewrite plus_n_Sm; auto. rewrite H4; simpl in |- *; ring. Qed.
imports: Coq(ArithRing) Bertrand(Misc)