proposition: Theorem sub_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. unfold Rminus. apply add_aa_o with xi yi. exact Hx. unfold ABS. rewrite Rabs_Ropp. exact Hy. exact Hb. Qed.
imports: Gappa_common Gappa_pred_nzr