proposition: Theorem nNormMimLtvNum : (nNormMin radix precision < pPred (vNum b))%Z.
proof: Proof. unfold pPred in |- *; rewrite PosNormMin with (radix := radix) (precision := precision); auto with zarith. apply Z.lt_le_trans with (Z.pred (2 * nNormMin radix precision)). replace (Z.pred (2 * nNormMin radix precision)) with (Z.pred (nNormMin radix precision) + nNormMin radix precision)%Z; [ idtac | unfold Z.pred in |- *; ring ]. pattern (nNormMin radix precision) at 1 in |- *; replace (nNormMin radix precision) with (0 + nNormMin radix precision)%Z; [ idtac | ring ]. apply Zplus_lt_compat_r; auto. apply Zlt_succ_pred. replace (Z.succ 0) with (Z_of_nat 1); [ idtac | simpl in |- *; auto ]. rewrite <- (Zpower_nat_O radix); unfold nNormMin in |- *. apply Zpower_nat_monotone_lt. assumption. now apply Nat.lt_succ_lt_pred. apply Zle_Zpred_Zpred. apply Zle_Zmult_comp_r; auto with zarith. apply Z.lt_le_incl; apply nNormPos; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz