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