proposition: Theorem spec_to_Z: forall n : bigZ, BigN.to_Z (BigZ.to_N n) = (Z.sgn (BigZ.to_Z n) * BigZ.to_Z n)%Z.
proof: Proof. intros n; case n; simpl; intros p; generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. intros p1 H1; case H1; auto. intros p1 H1; case H1; auto. Qed.
imports: BigN ZProperties ZDivFloor ZSig ZSigZAxioms ZMake Ring Lia