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