proposition: Lemma Z_div_nz_opp_full : forall a b:Z, b <> 0 -> a mod b <> 0 -> (-a)/b = -(a/b)-1.
proof: Proof. intros a b. zero_or_not b; [easy|]. intros; rewrite Z.div_opp_l_nz; auto. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms