proposition: Theorem spec_abs: forall x, to_Z (abs x) = Z.abs (to_Z x).
proof: Proof. intros x; case x; clear x; intros x; assert (F:=NN.spec_pos x). simpl; rewrite Z.abs_eq; auto. simpl; rewrite Z.abs_neq; simpl; auto with zarith. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig