proposition: Theorem add_aa_n : forall x y : R, forall xi yi zi : FF, ABS x xi -> ABS y yi -> add_aa_n_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 (Hb,H3). generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fpos0_correct _ H1). clear H1. intro H1. generalize (Fle2_correct _ _ H2). rewrite Fminus2_correct. clear H2. intro H2. generalize (Fle2_correct _ _ H3). rewrite Fplus2_correct. clear H3. intro H3. split. exact H1. split. apply Rle_trans with (Rabs y - Rabs x)%R. apply Rle_trans with (1 := H2). unfold Rminus. apply Rplus_le_compat with (1 := proj1 (proj2 Hy)). apply Ropp_le_contravar with (1 := proj2 (proj2 Hx)). replace (x + y)%R with (y - -x)%R. 2: ring. rewrite<- (Rabs_Ropp x). apply Rabs_triang_inv. apply Rle_trans with (Rabs x + Rabs y)%R. apply Rabs_triang. apply Rle_trans with (2 := H3). apply Rplus_le_compat with (1 := proj2 (proj2 Hx)) (2 := proj2 (proj2 Hy)). Qed.
imports: Gappa_common Gappa_pred_nzr