proposition: Lemma Zquot_Zquot : forall a b c, (a÷b)÷c = a÷(b*c).
proof: Proof. intros. zero_or_not b. rewrite Z.mul_comm. zero_or_not c. rewrite Z.mul_comm. apply Z.quot_quot; auto. Qed.
imports: Nnat ZArith_base Lia ZArithRing Zdiv Morphisms