proposition: Lemma Zmult_iden_l : forall x : Z, (1 * x) %= x.
proof: Proof. intros. ring_simplify; apply mod_eq_refl. Qed.
imports: Arith ZArith RelationClasses Type_class_definition Lia ZArith Znumtheory ZArith Znumtheory ConstructiveEpsilon