proposition: Theorem div_nn : forall x y : R, forall xi yi zi : FF, BND x xi -> BND y yi -> div_nn_helper xi yi zi = true -> BND (x / y) zi.
proof: Proof. intros x y xi yi zi Hx Hy Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (Hb,H4). generalize (andb_prop _ _ Hb). clear Hb. intros (Hb,H3). generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fneg_correct _ H1). clear H1. intro H1. generalize (Fneg0_correct _ H2). clear H2. intro H2. generalize (Fle2_correct _ _ H3). rewrite Fmult2_correct. clear H3. intro H3. generalize (Fle2_correct _ _ H4). rewrite Fmult2_correct. clear H4. intro H4. apply IRdiv_nn with (1 := H2) (2 := H1) (3 := H3) (4 := H4) (5 := Hx) (6 := Hy). Qed.
imports: Gappa_common Gappa_decimal