proposition: Lemma intP (x : Z) : Z_spec x x.
proof: Proof. destruct x as [|p|p]. - now apply ZintNull. - rewrite <-positive_nat_Z at 2. apply ZintPos. now rewrite positive_nat_Z. - rewrite <-Pos2Z.opp_pos. rewrite <-positive_nat_Z at 2. apply ZintNeg. now rewrite positive_nat_Z. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac