proposition: Lemma div_trans : forall p q r : nat, Divides p q -> Divides q r -> Divides p r.
proof: Proof. intros. elim H. elim H0. intros. unfold Divides in |- *. split with (x0 * x). rewrite H1. rewrite H2. rewrite mult_assoc. reflexivity. Qed.
imports: ZArith Wf_nat lemmas natZ dec exp