proposition: Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a.
proof: Proof. intros a b H H1;case (Z_mod_lt a b);auto with zarith;intros H2 H3;split;auto. case (Z.le_gt_cases b a); intros H4; auto with zarith. rewrite Zmod_small; auto with zarith. Qed.
imports: ArithRing ZArith Znumtheory Zpow_facts Lia