proposition: Lemma sgn_nonneg : forall n, 0 <= sgn n <-> 0 <= n.
proof: Proof. intros n; split. - destruct_sgn n; intros. + now apply lt_le_incl. + order. + elim (lt_irrefl 0). apply lt_le_trans with 1; auto using lt_0_1. now rewrite <- opp_nonneg_nonpos. - rewrite lt_eq_cases; destruct 1. + rewrite sgn_pos by auto. apply lt_le_incl, lt_0_1. + rewrite sgn_null by auto with relations. apply le_refl. Qed.
imports: ZMulOrder