proposition: Lemma Zdivides_antisymm : forall a b : Z, (a > 0)%Z -> (b > 0)%Z -> Zdivides a b -> Zdivides b a -> a = b.
proof: Proof. intros a b H01 H02 H1 H2. unfold Zdivides in H1; elim H1; intros q1 H1_. unfold Zdivides in H2; elim H2; intros q2 H2_. generalize H2_; intro H12_. rewrite <- H1_ in H12_. rewrite Zmult_assoc in H12_. rewrite Zmult_comm in H12_. rewrite <- H1_. rewrite <- (Zmult_1_l a). assert (Zdivides q1 1). replace 1%Z with (q2 * q1)%Z. apply Zdivides_mult_elim_lft. apply Zdivides_ref. apply (Zunit_eq_one (q2 * q1) a). auto with zarith. assumption. replace q1 with 1%Z. auto with zarith. symmetry in |- *. rewrite Zmult_comm in H1_; rewrite <- H1_ in H02. apply Zdiv_one_is_one; auto. apply (Zdiv_pos_pos a); auto. Qed.
imports: CoRN.model.Zmod.ZBasics