proposition: Theorem FweightLt : 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. cut (Fbounded b p); [ intros Fb1 | apply FcanonicBound with (1 := H') ]; auto. cut (Fbounded b q); [ intros Fb2 | apply FcanonicBound with (1 := H'0) ]; auto. case (FcanonicLtPos _ radixMoreThanOne b precision) with (p := p) (q := q); auto with arith; intros Zl1. unfold Fweight in |- *; simpl in |- *. replace (Fexp q) with (Fexp q - Fexp p + Fexp p)%Z; [ idtac | ring ]. rewrite Zmult_plus_distr_l. rewrite Zplus_assoc. repeat rewrite (fun x y z : Z => Zplus_comm x (y * z)). apply Zplus_lt_compat_l. apply Z.lt_le_trans with (Zpower_nat radix precision); auto with zarith. apply Z.le_lt_trans with (Z.pred (Zpower_nat radix precision)); auto with zarith. apply Zle_Zabs_inv2; auto with zarith. apply Zle_Zpred; auto with zarith. rewrite <- pGivesBound; apply Fb1. apply Z.le_trans with ((Fexp q - Fexp p) * Zpower_nat radix precision)%Z; auto with zarith. pattern (Zpower_nat radix precision) at 1 in |- *; replace (Zpower_nat radix precision) with (Z.succ 0 * Zpower_nat radix precision)%Z; auto. apply Zle_Zmult_comp_r; lia. unfold Z.succ in |- *; ring. cut (0 <= Fnum q)%Z; auto with zarith. apply (LeR0Fnum radix); auto. apply Rle_trans with (FtoRradix p); auto; apply Rlt_le; auto. elim Zl1; intros H'3 H'4; clear Zl1. unfold Fweight in |- *; simpl in |- *. rewrite <- H'3. repeat rewrite (fun x y z : Z => Zplus_comm x (y * z)). apply Zplus_lt_compat_l; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz