proposition: Lemma one_plus_correct : forall x xi, BND x xi -> BND (1 + x) (one_plus xi).
proof: Proof. intros x xi Hx. apply IRplus with (xl := 1%R) (xu := 1%R) (4 := Hx) ; simpl. rewrite Fplus2_correct. apply Rplus_le_compat_r. unfold float2R, Defs.F2R. simpl. rewrite Rmult_1_l. apply Rle_refl. rewrite Fplus2_correct. apply Rplus_le_compat_r. unfold float2R, Defs.F2R. simpl. rewrite Rmult_1_l. apply Rle_refl. split ; apply Rle_refl. Qed.
imports: Gappa_common Gappa_pred_bnd