proposition: Lemma Z_div_mult_full : forall a b:Z, b <> 0 -> (a*b)/b = a.
proof: Proof. Proof Z.div_mul. Lemma Z_div_pos: forall a b, b > 0 -> 0 <= a -> 0 <= a/b. Proof. intros. apply Z.div_pos; auto using Z.gt_lt. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms