proposition: Lemma pos_abs_comp : forall (x : Z) (p p' : (x > 0)%Z), pos_abs p = pos_abs p'.
proof: Proof. intros x; try assumption. elim x. intros p p'; try assumption. red in p'. inversion p. intros p p0 p'; simpl in |- *. auto with algebra. intros p p0 p'; try assumption. red in p'. simpl in p'. inversion p'. Qed.
imports: Z_group