proposition: Lemma Fle_Zle : forall n1 n2 d : Z, (n1 <= n2)%Z -> Fle (Float n1 d) (Float n2 d).
proof: Proof. intros; unfold Fle, FtoRradix, FtoR in |- *; simpl in |- *; auto. case Zle_lt_or_eq with (1 := H); intros H1. apply Rlt_le, Rmult_lt_compat_r. now apply powerRZ_lt, IZR_lt. apply IZR_lt; easy. rewrite <- H1; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz