Is there a way to “extend” prelude.pvs? For example, if I want to make the following proven lemma available to proofs in any theory without requiring them to have an IMPORTING statement for the helper lemma:
FORALL(a: real, nnx: nnreal, b: real, nny: nnreal):
abs(a) <= nnx AND abs(b) <= nny IMPLIES
-(nnx * nny) <= (a * b) AND
(a * b) <= (nnx * nny);
Is there a way to do this? I’ve tried renaming the containing file prelude.pvs (in the current working directory), but that did not do the job.