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