proposition: Lemma Zdiv_1_l: forall a, 1 < a -> 1/a = 0.
proof: Proof. Proof Z.div_1_l. Lemma Zmod_1_l: forall a, 1 < a -> 1 mod a = 1. Proof Z.mod_1_l. Lemma Z_div_same_full : forall a:Z, a<>0 -> a/a = 1. Proof Z.div_same. Lemma Z_mod_same_full : forall a, a mod a = 0. Proof. intros a. zero_or_not a. apply Z.mod_same; auto. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms