proposition: Lemma divides_antisym : forall a b : nat, divides a b -> divides b a -> a = b.
proof: Proof. intros a b; case a; case b; auto. intros b' (q1, H1) H2; rewrite H1; auto with arith. intros a' H1 (q2, H2); rewrite H2; auto with arith. intros b' a' H' H'0; apply Nat.le_antisymm; apply divides_le; auto. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)