proposition: Lemma nonneg_mant (x : Dyadic) : 0 ≤ x ↔ 0 ≤ mant x.
proof: Proof. split; intros E. unfold le, dy_le, DtoQ_slow in E. simpl in *. apply (order_reflecting ZtoStdQ). apply (order_reflecting (.* 2 ^ expo x)). now rewrite rings.preserves_0, left_absorb in E |- *. unfold le, dy_le, DtoQ_slow. simpl. apply (order_preserving ZtoStdQ) in E. apply (order_preserving (.* 2 ^ expo x)) in E. now rewrite rings.preserves_0, left_absorb in E |- *. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.naturals MathClasses.interfaces.rationals MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.orders.minmax MathClasses.orders.integers MathClasses.orders.rationals MathClasses.implementations.nonneg_integers_naturals MathClasses.implementations.stdlib_rationals MathClasses.theory.rationals MathClasses.theory.shiftl MathClasses.theory.int_pow MathClasses.theory.nat_pow MathClasses.theory.abs