proposition: Lemma Z2int_opp n : Z2int (- n) = (- (Z2int n))%R.
proof: Proof. by case n=>// p /=; rewrite GRing.opprK. Qed.
imports: ZArith QArith Lia Bignums(BigQ) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat order) mathcomp(ssralg ssrnum ssrint rat div intdiv) CoqEAL.refinements(hrel refinements param binint)