proposition: Lemma Zpos_pos_of_Z : forall a : Z, (0 < a)%Z -> (Zpos (pos_of_Z a) = a)%Z.
proof: Proof. induction a ; intros ; compute in H ; try discriminate H. exact (refl_equal _). Qed.
imports: Coq(ZArith Reals) Flocq(Zaux Raux Defs Digits Float_prop Generic_fmt FIX FLX) Gappa_definitions Gappa_dyadic