proposition: Lemma NatOfZ : forall n : Z, { p : nat | n = Z.of_nat p \/ n = Z.opp (Z.of_nat p) }.
proof: Proof. intros [|p|n]. - exists O. left. reflexivity. - exists (Pos.to_nat p). left. rewrite positive_nat_Z. reflexivity. - exists (Pos.to_nat n). right. rewrite positive_nat_Z. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs