proposition: Lemma pos_abs_ok : forall (x : Z) (px : (x > 0)%Z), x = Zpos (pos_abs px).
proof: Proof. intros x; try assumption. elim x. intros px; red in px. simpl in px. inversion px. simpl in |- *. auto with *. intros p px; red in px. simpl in px. inversion px. Qed.
imports: Zring Group_kernel