proposition: Lemma a_very_specific_lemma4 : forall a b c m n p : Z, ((a * (n * p) + (b * p + c * n) * m) * (m * n * p))%Z = (((a * n + b * m) * p + c * (m * n)) * (m * (n * p)))%Z.
proof: Proof. intros. ring. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq.Setoids.Setoid