proposition: Lemma rel_swap : forall x y e ei, BND e ei -> x = (y * (1 + e))%R -> Fpos (lower (one_plus ei)) = true -> y = (x / (1 + e))%R.
proof: Proof. intros x y e ei He Hx Hb. rewrite Hx. field. apply Rgt_not_eq. apply Rlt_gt. assert (H := one_plus_correct _ _ He). destruct H as (H,_). apply Rlt_le_trans with (2 := H). now apply Fpos_correct. Qed.
imports: Gappa_common Gappa_pred_bnd