proposition: Lemma error_of_rel_generic : forall f, forall t: (forall x y : R, forall xi yi zi : FF, BND x xi -> BND y yi -> f xi yi zi = true -> BND (x * y) zi), forall a b : R, forall xi yi zi : FF, REL a b xi -> BND b yi -> f xi yi zi = true -> BND (a - b) zi.
proof: Proof. intros f t a b xi yi zi (x,(Hr1,Hr2)). replace (a - b)%R with (x * b)%R. now apply t. rewrite Hr2. ring. Qed.
imports: Gappa_common Gappa_pred_bnd