proposition: Lemma div_rem0 : forall n d q r : nat, n = q * d + r -> r < d -> Divides d n -> r = 0.
proof: Proof. intros. elim H1. intros. rewrite H2 in H. rewrite (mult_comm q d) in H. apply (le_diff0 (d * q) (d * x)). apply le_mult_l. apply le_S_n. change (x < S q) in |- *. apply simpl_lt_mult_l with d. rewrite <- (mult_n_Sm d q). replace (d * x) with (d * q + r). apply plus_lt_compat_l. assumption. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ dec exp