proposition: Theorem nzr_of_nzr_rel : forall z zr : R, forall zi : FF, NZR zr -> REL z zr zi -> Flt2_m1 (lower zi) = true -> NZR z.
proof: Proof. intros z zr zi Hn (ze,(Hz1,Hz2)) H1. apply Flt2_m1_correct in H1. rewrite Hz2. apply prod_neq_R0. exact Hn. apply Rgt_not_eq. apply Rlt_le_trans with (1 + lower zi)%R. rewrite <- (Rplus_opp_r 1). apply Rplus_lt_compat_l. exact H1. apply Rplus_le_compat_l. apply Hz1. Qed.
imports: Gappa_common