proposition: Lemma one_mod_neutral_r : forall x, x * 1 == x.
proof: Proof. unfold equiv, mod_equiv, mod_eq, mult_op, mod_op, mult_mod. intro x; rewrite N.mul_1_r, N.mod_mod; auto with chains. Qed.
imports: Monoid_def RelationClasses Morphisms ZArith PArith Arith NArith Ring63