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