proposition: Lemma opp_inject_Z : forall n : Z, inject_Z (-n) == - inject_Z n.
proof: Proof. intros n; unfold inject_Z. setoid_replace (-n # 1)%Q with (-(n#1))%Q. - rewrite opp_inject_Q; reflexivity. - reflexivity. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra