proposition: Theorem sub_flt_rev : forall x y xn yn xyi zn, FLT x xn -> FLT y yn -> REL x y xyi -> sub_flt_helper xn yn zn xyi = true -> FLT (y - x) zn.
proof: Proof. intros x y xn yn xyi zn Hx Hy Hxy Hb. apply <- FLT_iff_generic. rewrite <- Ropp_minus_distr. apply generic_format_opp. apply -> FLT_iff_generic. eapply sub_flt ; eassumption. Qed.
imports: Flocq(Core Sterbenz) Gappa_common Gappa_round_aux