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