proposition: Lemma Zdiv_Zdiv : forall a b c, 0<=b -> 0<=c -> (a/b)/c = a/(b*c).
proof: Proof. intros a b c ? ?. zero_or_not b. rewrite Z.mul_comm. zero_or_not c. rewrite Z.mul_comm. apply Z.div_div; auto. apply Z.le_neq; auto. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms