proposition: Theorem sub_fix : forall x y : R, forall xn yn zn : Z, FIX x xn -> FIX y yn -> add_fix_helper xn yn zn = true -> FIX (x - y)%R zn.
proof: Proof. intros x y xn yn zn Hx (fy,(Hy1,Hy2)) Hb. unfold Rminus. apply (add_fix _ (-y) _ yn zn Hx). exists (Fopp2 fy). split. rewrite <- Hy1. apply Fopp2_correct. exact Hy2. exact Hb. Qed.
imports: Flocq(Core Sterbenz) Gappa_common Gappa_round_aux