proposition: Lemma spec_Zabs_N : forall z, BigN.to_Z (Zabs_N z) = Z.abs (BigZ.to_Z z).
proof: Proof. unfold Zabs_N; intros. rewrite BigZ.spec_to_Z, Z.mul_comm; apply Z.sgn_abs. Qed.
imports: BigZ Field Qfield QSig QMake Orders GenericMinMax