proposition: Theorem add_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 (fx,(Hx1,Hx2)) (fy,(Hy1,Hy2)) Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Zle_bool_imp_le _ _ H1). clear H1. intro H1. generalize (Zle_bool_imp_le _ _ H2). clear H2. intro H2. exists (Fplus2 fx fy). split. rewrite <- Hx1. rewrite <- Hy1. apply Fplus2_correct. unfold Fplus2, Fshift2. case (Fexp fx - Fexp fy)%Z ; intros. exact (Z.le_trans _ _ _ H1 Hx2). exact (Z.le_trans _ _ _ H2 Hy2). exact (Z.le_trans _ _ _ H1 Hx2). Qed.
imports: Flocq(Core Sterbenz) Gappa_common Gappa_round_aux