proposition: Lemma Zdiv_POS : forall a b : positive, (Zpos b * (Zpos a / Zpos b) <= Zpos a)%Z.
proof: Proof. intros a b. rewrite <- (Zplus_0_r (Zpos b * (Zpos a / Zpos b))). set (lhs := (Zpos b * (Zpos a / Zpos b) + 0)%Z) in *. rewrite (Z_div_mod_eq_full (Zpos a) (Zpos b)). unfold lhs in |- *. apply Zplus_le_compat_l. auto with zarith. generalize (Z_mod_lt (Zpos a) (Zpos b)). intro H. elim H. auto with zarith. auto with zarith. Qed.
imports: CoRN.model.Zmod.ZBasics