proposition: Theorem div_divides_S : forall p q : nat, 0 < q -> divides q (S p) -> div (S p) q = S (div p q).
proof: Proof. intros p q H (qr, H1); apply sym_equal; auto. apply trans_equal with qr. generalize (pdiv_def p q H); unfold div in |- *; case (pdiv p q); simpl in |- *. intros q1 r1 (H2, H3). apply eq_mult with q; auto with arith. apply sym_not_equal; auto with arith. repeat rewrite (Nat.mul_comm q); auto with arith. rewrite <- H1; rewrite H2. cut (S r1 = q); [ intros H4 | idtac ]. rewrite plus_n_Sm; rewrite H4; simpl in |- *; ring. apply Nat.le_antisymm; auto with arith. apply divides_le; auto with arith. apply divides_plus2 with (b := q1 * q). exists q1; auto with arith. rewrite <- plus_n_Sm; rewrite <- H2; auto. rewrite H1; exists qr; auto. apply div_unique; auto with arith. rewrite H1; rewrite (Nat.mul_comm q); auto with arith. rewrite H1; repeat rewrite (Nat.mul_comm qr); auto with arith. Qed.
imports: Coq(ArithRing) Bertrand(Misc)