proposition: Theorem pdiv_aux_def : forall m n p : nat, m <= p -> 0 < n -> match pdiv_aux m n p with | (q, r) => m = q * n + r /\ r < n end.
proof: Proof. intros m n p; generalize m n; clear m n; elim p; clear p; simpl in |- *. intros m n H; inversion H; simpl in |- *; case n; simpl in |- *; auto with arith. intros p1 Rec m n H1 H2. generalize (ominus_def m n); case (ominus m n); auto with arith. intros s Hs; generalize (Rec s n); case (pdiv_aux s n p1). intros q r H3; case H3; auto with arith. apply Nat.lt_succ_r. apply Nat.lt_le_trans with (2 := H1). rewrite Hs. pattern s at 1 in |- *; replace s with (0 + s); auto with arith. intros H4 H5; split; auto. rewrite Hs; rewrite H4; simpl in |- *; auto with arith. Qed.
imports: Coq(ArithRing) Bertrand(Misc)