proposition: Theorem sub_rr : forall x1 x2 y1 y2 : R, forall xi yi qi zi : FF, REL x1 x2 xi -> REL y1 y2 yi -> BND (x2 / (x2 - y2)) qi -> NZR (x2 - y2) -> add_rr_helper xi yi qi zi = true -> REL (x1 - y1) (x2 - y2) zi.
proof: Proof. intros x1 x2 y1 y2 xi yi qi zi Hx (ey,(Hy1,Hy2)) Hq Zxy Hb. apply add_rr with (1 := Hx) (3 := Hq) (4 := Zxy) (5 := Hb). exists ey. split. exact Hy1. rewrite Hy2. ring. Qed.
imports: Gappa_common Gappa_pred_bnd