proposition: Lemma a_very_specific_lemma2 : forall a b c d s r t u : Z, (a * r)%Z = (b * s)%Z -> (c * u)%Z = (d * t)%Z -> ((a * t + c * s) * (r * u))%Z = ((b * u + d * r) * (s * t))%Z.
proof: Proof. intros. replace ((a * t + c * s) * (r * u))%Z with (a * r * t * u + c * u * s * r)%Z by ring. rewrite H in |- *; rewrite H0 in |- *; ring. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq.Setoids.Setoid