proposition: Theorem div_rem : forall d n : nat, d > 0 -> exists q : nat, (exists r : nat, 0 <= r /\ r < d /\ n = q * d + r).
proof: Proof. intros d n. apply (lt_wf_ind n). intros N IH. intros. elim (le_or_lt d N). intro. elim (le_witness d N). intros x Hx. elim (IH x). intro q'. intros. elim H1. intro r'. intros. elim H2. intros. elim H4. intros. split with (S q'). split with r'. split. assumption. split. assumption. simpl in |- *. rewrite <- Hx. rewrite (plus_assoc_reverse d (q' * d)). rewrite <- H6. reflexivity. unfold lt in |- *. apply witness_le. split with (pred d). rewrite plus_Snm_nSm. rewrite <- (S_pred d 0). rewrite plus_comm. assumption. assumption. assumption. assumption. intro. split with 0. split with N. split. apply le_O_n. split. assumption. simpl in |- *. reflexivity. Qed.
imports: ZArith Wf_nat lemmas natZ dec exp