proposition: Fact ex10 : (0 <= p)%Z -> FTZ_format r e p 0.
proof: Proof. intros Ppos. exists {| Fnum := 0; Fexp := e |}; simpl. - unfold F2R; simpl; ring. - intro HH; destruct HH; auto. - lia. Qed.
imports: Psatz ZArith Reals Flocq(FTZ Core Operations)