proposition: Lemma div_antisym : forall a b : nat, Divides a b -> Divides b a -> a = b.
proof: Proof. intros. elim H. elim H0. intros x Ha y Hb. rewrite Hb in Ha. rewrite mult_assoc_reverse in Ha. elim (mult_ppq_p0q1 a (y * x)). intro. rewrite H1 in Hb. simpl in Hb. rewrite H1. rewrite Hb. reflexivity. intros. elim (mult_pq1_p1q1 y x H1). intros. rewrite H2 in Hb. rewrite <- mult_n_Sm in Hb. rewrite <- mult_n_O in Hb. simpl in Hb. symmetry in |- *. assumption. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ dec exp