proposition: Lemma div_pred : forall x y q : nat, 0 < x -> is_div x y q 0 -> is_div (pred x) y (pred q) (pred y).
proof: Proof. intros x y q H' (H'1, H'2); split; auto. generalize H'1; case y; simpl in |- *; auto with arith. rewrite H'2; auto. rewrite <- plus_n_O; auto. generalize H'2; case q; simpl in |- *; auto. intros H'3; Contradict H'; auto with arith. rewrite H'3; auto with arith. intros n H'3; generalize H'1; case y; simpl in |- *; auto with arith. intros H'4; Contradict H'4; auto with arith. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)