proposition: Theorem add_aa_o : forall x y : R, forall xi yi zi : FF, ABS x xi -> ABS y yi -> add_aa_o_helper xi yi zi = true -> ABS (x + y) zi.
proof: Proof. intros x y xi yi zi Hx Hy Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fis0_correct _ H1). clear H1. intro H1. generalize (Fle2_correct _ _ H2). rewrite Fplus2_correct. clear H2. intro H2. split. auto with real. split. rewrite H1. apply Rabs_pos. apply Rle_trans with (Rabs x + Rabs y)%R. apply Rabs_triang. apply Rle_trans with (2 := H2). apply Rplus_le_compat with (1 := proj2 (proj2 Hx)) (2 := proj2 (proj2 Hy)). Qed.
imports: Gappa_common Gappa_pred_nzr