proposition: Lemma rnz_ler z1 z2 : (z1 <= z2)%R -> rnz z1 <= rnz z2.
proof: Proof. rewrite /rnz; case: ler0P => // z1_gt0 z1Lz2; case: ler0P => //= [|z2_gt0]. by rewrite leNgt => /negP[]; apply: lt_le_trans z1Lz2. by rewrite -lez_nat !gtz0_abs. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)