proposition: Lemma Zdiv_lt_POS : forall a b : positive, (Zpos a < Zpos b)%Z -> (Zpos a / Zpos b)%Z = 0%Z.
proof: Proof. intros a b Hlt. apply (Zdiv_quotient_unique (Zpos a) (Zpos b) (Zpos a / Zpos b) (Zpos a mod Zpos b) 0 (Zpos a)); auto with zarith. rewrite Zmult_comm. apply Z_div_mod_eq_full. apply Z_mod_lt; auto with zarith. Qed.
imports: CoRN.model.Zmod.ZBasics