proposition: Theorem FweightZle : forall p q : float, Fcanonic radix b p -> Fcanonic radix b q -> (0 <= p)%R -> (p <= q)%R -> (Fweight p <= Fweight q)%Z.
proof: Proof. intros p q H' H'0 H'1 H'2; Casec H'2; intros H'2. apply Zlt_le_weak. apply FweightLt; auto. rewrite (FweightEq p q); auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz