All presented properties are showed by automated theorem-prover Prover9.
(There is no special order in the presentation of the theorems.)

ID	Name	Lemma	Duals
FA1	refinement is a preorder	$x\rord x \wedge(x\rord y \wedge y\rord z \Rightarrow x\rord z)$	n/a
FA2	natural order implies refinement	$x\leq y \Rightarrow x\rord y$	n/a
FA3	infima and suprema of refinement	$x;y\rord y$ $x\rord x+y$	n/a
FA4	isotony w.r.t. refinement and addition	$x\rord y \Rightarrow x+z\rord y+z$	$x\rord y \Rightarrow z+x\rord z+y$
FA5	isotony w.r.t. refinement and multiplication	$x\rord y \Rightarrow x\cdot z\rord y\cdot z$	$x\rord y \Rightarrow z\cdot x\rord z\cdot y$
FA6	strictness of refinement order	$(x\rord 0 \Leftrightarrow x=0) \wedge (x\rord 0 \Leftrightarrow x\leq0)$	n/a
FA7	least and greatest element w.r.t. refinement	$0\rord x$ $x\rord 1$	n/a
FA8	refinement equivalence I	$x\rord y \Rightarrow x\leq y\cdot \top$	n/a
FA9	refinement equivalence II	$x\rord y \Leftarrow x\leq y\cdot \top$	n/a
FA10	ideal equivalence I	$x\leq y\cdot \top \Rightarrow x\cdot \top\leq y\cdot\top$	n/a
FA11	ideal equivalence II	$x\leq y\cdot \top\top \Leftarrow x\cdot \top\leq y\cdot\top$	n/a
FA12	antisymmetry	$\forall x \forall y(x\rord y \wedge y\rord x \Rightarrow x=y) \Leftarrow \forall x \forall y (x\rord y \Rightarrow x=y)$	n/a
FA13	join splitting I	$x+y\rord z \Rightarrow x\rord z \wedge y\rord z$	n/a
FA14	join splitting II	$x+y\rord z \Leftarrow x\rord z \wedge y\rord z$	n/a
FA15	requirement relation is reflexive	$p\pims p$	n/a
FA16	requirement relation is transitive	$(p\pims q \wedge q\pims r)\Rightarrow p\pims r$	n/a

In general, we write $x,y...$ and $a,b...$ for arbitrary semiring elements and $p,q...$ for tests. If other letters are involved we adapted the original notation of the authors.