proposition: Theorem oneExp_le : forall x y : Z, (x <= y)%Z -> (Float 1 x <= Float 1 y)%R.
proof: Proof. intros x y H'; unfold FtoR in |- *; simpl in |- *. repeat rewrite Rmult_1_l; auto with real zarith. apply Rle_powerRZ; try replace 1%R with (IZR 1); auto with real zarith zarith. apply IZR_le; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz