proposition: Lemma div_minus_compat : forall a b d : nat, Divides d a -> Divides d b -> Divides d (a - b).
proof: Proof. intros. elim H. elim H0. intros. unfold Divides in |- *. rewrite H1. rewrite H2. rewrite (mult_comm d). rewrite (mult_comm d). rewrite <- mult_minus_distr_r. split with (x0 - x). apply mult_comm. Qed.
imports: ZArith Wf_nat lemmas natZ dec exp