proposition: Lemma quot_1_r: forall a, a÷1 == a.
proof: Proof. intros a. pos_or_neg a. - now apply NZQuot.div_1_r. - apply opp_inj. rewrite <- quot_opp_l. + apply NZQuot.div_1_r; order. + intro EQ; symmetry in EQ; revert EQ; apply lt_neq, lt_0_1. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv