proposition: Lemma div_refl : forall x : R, forall zi : FF, NZR x -> div_refl_helper zi = true -> BND (x / x) zi.
proof: Proof. intros x zi Hx Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). assert (Float2 1 0 = 1 :>R)%R. apply Rmult_1_r. generalize (Fle2_correct _ _ H1). clear H1. rewrite H. intro H1. generalize (Fle2_correct _ _ H2). clear H2. rewrite H. intro H2. unfold Rdiv. rewrite Rinv_r. 2: exact Hx. exact (conj H1 H2). Qed.
imports: Gappa_common Gappa_decimal