proposition: Theorem notdiv_rem : forall d n : nat, 0 < d -> ~ Divides d n -> exists q : nat, (exists r : nat, 0 < r /\ r < d /\ n = q * d + r).
proof: Proof. intros d n. elim (le_or_lt d n). intro. elim (le_lt_or_eq d n). apply (lt_wf_ind n). intros N IH. intros. elim (lt_witness d N). intros. elim H3. intros. elim (le_or_lt d x). intro. elim (le_lt_or_eq d x). intro. elim (divdec x d). intros. elim H8. intros. rewrite H9 in H4. rewrite plus_comm in H4. rewrite mult_n_Sm in H4. elim H2. split with (S x0). symmetry in |- *. assumption. intros. elim (IH x). intro q'. intros. elim H9. intro r'. intros. elim H10. intros. elim H12. intros. split with (S q'). split with r'. split. assumption. split. assumption. simpl in |- *. rewrite plus_assoc_reverse. rewrite <- H14. symmetry in |- *. assumption. rewrite <- H4. pattern x at 1 in |- *. replace x with (0 + x). apply plus_lt_compat_r. assumption. simpl in |- *. reflexivity. assumption. assumption. assumption. intro. elim H2. split with 2. rewrite mult_comm. simpl in |- *. rewrite <- (plus_n_O d). rewrite <- H4. rewrite H7. reflexivity. assumption. intro. split with 1. split with x. split. assumption. split. assumption. simpl in |- *. rewrite <- (plus_n_O d). rewrite H4. reflexivity. assumption. intros. elim H2. split with 1. rewrite mult_comm. simpl in |- *. rewrite <- (plus_n_O d). symmetry in |- *. assumption. assumption. case n. intros. elim H1. split with 0. apply mult_n_O. intro n1. intros. split with 0. split with (S n1). split. apply lt_O_Sn. split. assumption. simpl in |- *. reflexivity. Qed.
imports: ZArith Wf_nat lemmas natZ dec exp