proposition: Theorem bnd_of_rel_bnd_n : forall x y : R, forall xi ei yi : FF, BND x xi -> REL x y ei -> div_np_helper xi (one_plus ei) yi = true -> BND y yi.
proof: Proof. intros x y yi ei xi Hy (e,(He1,He2)) Hb. destruct (andb_prop _ _ Hb) as (H1,_). generalize (andb_prop _ _ H1). clear H1. intros (H1,_). generalize (andb_prop _ _ H1). clear H1. intros (H1,_). rewrite rel_swap with (1 := He1) (2 := He2) (3 := H1). apply div_np with (1 := Hy) (3 := Hb). apply one_plus_correct with (1 := He1). Qed.
imports: Gappa_common Gappa_pred_bnd