proposition: Lemma rem_1_r: forall a, a rem 1 == 0.
proof: Proof. intros. rewrite rem_eq, quot_1_r; nzsimpl; auto using sub_diag. intro EQ; symmetry in EQ; revert EQ; apply lt_neq; apply lt_0_1. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv